Theorem abeq2 2315

Description: Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbi 2320 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable.

Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable 𝜑 (that has a free variable 𝑥) to a theorem with a class variable 𝐴, we substitute 𝑥 ∈ 𝐴 for 𝜑 throughout and simplify, where 𝐴 is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable 𝐴 to one with 𝜑, we substitute {𝑥 ∣ 𝜑} for 𝐴 throughout and simplify, where 𝑥 and 𝜑 are new set and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
abeq2	⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abeq2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-17 1550	. . 3 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
2		hbab1 2195	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → ∀𝑥 𝑦 ∈ {𝑥 ∣ 𝜑})
3	1, 2	cleqh 2306	. 2 ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}))
4		abid 2194	. . . 4 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
5	4	bibi2i 227	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}) ↔ (𝑥 ∈ 𝐴 ↔ 𝜑))
6	5	albii 1494	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))
7	3, 6	bitri 184	1 ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑))

Syntax hints:   ↔ wb 105  ∀wal 1371   = wceq 1373   ∈ wcel 2177  {cab 2192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202

This theorem is referenced by:  abeq1  2316  abbi2i  2321  abbi2dv  2325  clabel  2333  sbabel  2376  rabid2  2684  ru  3001  sbcabel  3084  ssalel  3185  vpwex  4234  dmopab3  4905