Theorem abeq2 1568

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 1573 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 ph (that has a free variable x) to a theorem with a class variable A, we substitute x e. A for ph throughout and simplify, where A is a new class variable not already in the wff. An example is the conversion of zfauscl 2705 to inex1 2716 (look at the instance of zfauscl 2705 that occurs in the proof of inex1 2716). Conversely, to convert a theorem with a class variable A to one with ph, we substitute {x | ph} for A throughout and simplify, where x and ph are new set and wff variables not already in the wff. An example is cp 4722, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 4721.

Assertion

Ref	Expression
abeq2	|- (A = {x | ph} <-> A.x(x e. A <-> ph))

Distinct variable group:   x,A

Proof of Theorem abeq2

Step	Hyp	Ref	Expression
1		ax-17 971	. . 3 |- (y e. A -> A.x y e. A)
2		hbab1 1466	. . 3 |- (y e. {x | ph} -> A.x y e. {x | ph})
3	1, 2	cleqf 1560	. 2 |- (A = {x | ph} <-> A.x(x e. A <-> x e. {x | ph}))
4		abid 1465	. . . 4 |- (x e. {x | ph} <-> ph)
5	4	bibi2i 608	. . 3 |- ((x e. A <-> x e. {x | ph}) <-> (x e. A <-> ph))
6	5	albii 999	. 2 |- (A.x(x e. A <-> x e. {x | ph}) <-> A.x(x e. A <-> ph))
7	3, 6	bitr 173	1 |- (A = {x | ph} <-> A.x(x e. A <-> ph))

Syntax hints:   <-> wb 146  A.wal 954   = wceq 956   e. wcel 958  {cab 1463

This theorem is referenced by:  abeq1 1569  abbi2i 1574  abbi2dv 1578  clabel 1582  sbabel 1584  rabid2 1770  ru 1938  sbcabel 1996  sbcel12g 2011  dfss2 2058  ssequn1 2200  zfrep4 2701  pwex 2745  dmopab3 3322  funimaexg 3575  difeqri2 10443

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472

Copyright terms: Public domain