Theorem abeq2 1836

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 1841 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 3255 to inex1 3267 (look at the instance of zfauscl 3255 that occurs in the proof of inex1 3267). 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 5648, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 5647.

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 1155	. . 3 |- (y e. A -> A.x y e. A)
2		hbab1 1711	. . 3 |- (y e. {x | ph} -> A.x y e. {x | ph})
3	1, 2	cleqf 1821	. 2 |- (A = {x | ph} <-> A.x(x e. A <-> x e. {x | ph}))
4		abid 1710	. . . 4 |- (x e. {x | ph} <-> ph)
5	4	bibi2i 666	. . 3 |- ((x e. A <-> x e. {x | ph}) <-> (x e. A <-> ph))
6	5	albii 1184	. 2 |- (A.x(x e. A <-> x e. {x | ph}) <-> A.x(x e. A <-> ph))
7	3, 6	bitri 189	1 |- (A = {x | ph} <-> A.x(x e. A <-> ph))

Syntax hints:   <-> wb 162  A.wal 1134   = wceq 1136   e. wcel 1138  {cab 1708

This theorem is referenced by:  abeq1 1837  abbi2i 1842  abbi2dv 1846  clabel 1851  sbabel 1853  rabid2 2087  rabid2OLD 2088  ru 2284  sbcabel 2368  sbcel12gOLD 2386  dfss2 2443  ssequn1OLD 2606  zfrep4 3251  pwex 3302  pwexOLD 3303  dmopab3 3980  funimaexg 4306  usinuniop 10133  cbicplem 14234

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-10 1146  ax-12 1148  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702

This theorem depends on definitions:  df-bi 163  df-an 241  df-ex 1165  df-sb 1374  df-clab 1709  df-cleq 1714  df-clel 1717

Copyright terms: Public domain