Theorem abeq2 1571

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 1576 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 2711 to inex1 2722 (look at the instance of zfauscl 2711 that occurs in the proof of inex1 2722). 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 4739, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 4738.

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 973	. . 3 |- (y e. A -> A.x y e. A)
2		hbab1 1469	. . 3 |- (y e. {x | ph} -> A.x y e. {x | ph})
3	1, 2	cleqf 1563	. 2 |- (A = {x | ph} <-> A.x(x e. A <-> x e. {x | ph}))
4		abid 1468	. . . 4 |- (x e. {x | ph} <-> ph)
5	4	bibi2i 610	. . 3 |- ((x e. A <-> x e. {x | ph}) <-> (x e. A <-> ph))
6	5	albii 1001	. 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 956   = wceq 958   e. wcel 960  {cab 1466

This theorem is referenced by:  abeq1 1572  abbi2i 1577  abbi2dv 1581  clabel 1585  sbabel 1587  rabid2 1773  ru 1941  sbcabel 2000  sbcel12g 2015  dfss2 2062  ssequn1 2204  zfrep4 2707  pwex 2752  dmopab3 3329  funimaexg 3582  difeqri2 10446

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475

Copyright terms: Public domain