Qx∈E, A(x)
where A(x) abbreviates the formula defining A, whose free variables are x and possible parameters.(∀x∈E, A(x)) ⇔ {x∈E  A(x)} = E.
The one of firstorder logic can be defined in set theoretical interpretations, seeing A as a function and its Boolean values as objects:(∀x, A(x)) ⇔ A = (x ↦ 1)
Anyway (∀x, 1) is always true.(∃_{C } x, A(x))  ⇔ (∃x, C(x) ∧ A(x)) ⇔ ∃_{C∧A} x, 1 
(∀_{C } x, A(x))  ⇔ (∀x, C(x) ⇒ A(x)) 
∀x, C(x)  ⇔ ∃_{C } y, x=y 
(∀_{B}
x, C(x)) ⇒ (∀_{A} x,
C(x))
(∃_{A} x, C(x)) ⇒ (∃_{B}
x, C(x))
(∃_{C }x, A(x)) ⇒ (∃_{C
}x, B(x))
(∀_{C }x, A(x)) ⇒ (∀_{C
}x, B(x))
Existential Elimination. If ∃x, A(x), then we can introduce a new free variable z with the hypothesis A(z) (the consequences will be true without restricting the generality).
These rules express the meaning of ∃ : going from some term to ∃ then from ∃ to z, amounts to letting z represent that term (without knowing which, but they can be gathered into one by the conditional operator). They give the same meaning to ∃_{C } as to its 2 above equivalent formulas, bypassing (making implicit) the extended definiteness rule for (C ∧ A) by focusing on the case when C(x) is true and thus A(x) is definite.While ∃ appeared as the designation of an object, ∀ appears as a deduction rule: ∀_{C }x, A(x) means that its negation ∃_{C }x, ¬A(x) leads to a contradiction.
Universal Introduction. If from the mere hypothesis C(x) on a new free variable x we could deduce A(x), then ∀_{C }x, A(x).Universal Elimination. If ∀_{C }x, A(x) and t is a term satisfying C(t), then A(t).
Introducing then eliminating ∀ is like replacing x by t in the initial proof.These rules can be used to justify the following logically valid formulas
((∀_{C }x, A(x))
∧ (∀_{C }x, A(x) ⇒ B(x)))
⇒ (∀_{C }x, B(x))
((∃_{C }x, A(x))
∧ (∀_{C }x, A(x) ⇒ B(x)))
⇒ (∃_{C }x, B(x))
((∀_{C }x, A(x))
∧ (∃_{C }x, B(x))) ⇒
(∃_{C }x, A(x) ∧
B(x))
(∀_{C }x,
A(x)∨B(x)) ⇒ ((∀_{C }x,
A(x)) ∨ (∃_{C }x,
B(x)))
(∃_{A} x, ∀_{B}
y, R(x,y)) ⇒ (∀_{B} y,
∃_{A} x, R(x,y))
∀x, (∀y, R(x,y)) ⇒
R(x,x) ⇒ (∃y, R(x,y))
Secondorder Universal Introduction. If T'⊢F then T entails the secondorder statement (∀s, F(s)).
This holds for any model and the full set theoretical range of s, independently of the universe in which models and structures s are searched for.Secondorder Universal Elimination. Once a secondorder statement (∀s, F(s)) is accepted in a theory T, it is manifested in firstorder logic as a schema of statements, that is an infinite list of statements of the form (∀parameters, F(s)) for each possible replacement of s by a defining expression with parameters.
Applying secondorder universal elimination after secondorder universal introduction, means deducing from T a schema of theorems, each one indeed deducible in firstorder logic by the proof obtained from the original proof by replacing s by its definition.∀A, (Bx, A(x)) = F(A)
By secondorder universal elimination, this comes down to a schema of definitions in firstorder logic : for each expression defining A, it defines (Bx, A(x)) like a structure symbol, by the expression F(A) whose available free variables are the parameters of F plus those of A.Formula 3. ∀x,∀y, x = y ⇒ y = x 4. ∀x, ∀y, ∀z, (x = y ∧ y = z) ⇒ x = z 5. ∀f, ∀x, ∀y, x = y ⇒ f(x) = f(y) 6. ∀A, ∀x, ∀y, x = y ⇒ (A(x) ⇔ A(y)) 7. ∀x, ∀y, ∀z, (x = y ∧ z = y) ⇒ z = x 
Name
Symmetry Transitivity 
A(u) used
y = u u = z f(u) = f(y) ¬A(u) z = u 
Another possible list of axioms of equality consists in formulas 1. to 5. where f and A range over the mere symbols of the language, each taken once per argument : the full scheme of 2. is implied by successive deductions for each occurrence of symbol in A. This will be further justified in 2.11 (equivalence relations).
Introducing a variable x defined by a term t by writing (x = t ⇒ ...), in other words putting the axiom x = t, can be seen as justified by the above rules in this way : t = t ∴ ∃x, (x = t ∴ ...).
Set theory and Foundations of Mathematics  
1. First
foundations of mathematics 

Philosophical
aspects ⇨ Time in model theory 

2. Set theory  3. Algebra  4. Arithmetic  5. Secondorder foundations 