Theorem abeq2 1544

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 eq2ab 1549 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 x) to a theorem with a class variable A, we substitute x ∈ A for φ throughout and simplify, where A is a new class variable not already in the wff. An example is the conversion of zfauscl 2673 to inex1 2684 (look at the instance of zfauscl 2673 that occurs in the proof of inex1 2684). Conversely, to convert a theorem with a class variable A to one with φ, we substitute {x∣φ} for A throughout and simplify, where x and φ are new set and wff variables not already in the wff. An example is cp 4646, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 4645.

Assertion

Ref	Expression
abeq2	⊢ (A = {x∣φ} ↔ ∀x(x ∈ A ↔ φ))

Distinct variable group:   x,A

Proof of Theorem abeq2

Step	Hyp	Ref	Expression
1		ax-17 1190	. . 3 ⊢ (y ∈ A → ∀x y ∈ A)
2		hbab1 1443	. . 3 ⊢ (y ∈ {x∣φ} → ∀x y ∈ {x∣φ})
3	1, 2	cleqf 1536	. 2 ⊢ (A = {x∣φ} ↔ ∀x(x ∈ A ↔ x ∈ {x∣φ}))
4		abid 1442	. . . 4 ⊢ (x ∈ {x∣φ} ↔ φ)
5	4	bibi2i 606	. . 3 ⊢ ((x ∈ A ↔ x ∈ {x∣φ}) ↔ (x ∈ A ↔ φ))
6	5	albii 975	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ {x∣φ}) ↔ ∀x(x ∈ A ↔ φ))
7	3, 6	bitr 173	1 ⊢ (A = {x∣φ} ↔ ∀x(x ∈ A ↔ φ))

Syntax hints:   ↔ wb 146  ∀wal 950   = wceq 1099   ∈ wcel 1105  {cab 1440

This theorem is referenced by:  abeq1 1545  abbi2i 1550  abbi2dv 1554  clabel 1558  sbabel 1560  rabid2 1746  ru 1909  sbcabel 1967  sbcel12g 1982  dfss2 2029  ssequn1 2171  zfrep4 2669  pwex 2713  dmopab3 3279  funimaexg 3515  difeqri2 8703

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449

Copyright terms: Public domain