MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abeq2 Structured version   Unicode version

Theorem abeq2 2581
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 2588 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 4580 to inex1 4597 (look at the instance of zfauscl 4580 that occurs in the proof of inex1 4597). 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 setvar and wff variables not already in the wff. Examples include dfsymdif2 3732 and cp 8326; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 8325. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 26-May-1993.)

Assertion
Ref Expression
abeq2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem abeq2
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ax-5 1705 . . 3  |-  ( y  e.  A  ->  A. x  y  e.  A )
2 hbab1 2445 . . 3  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2cleqh 2572 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  x  e.  { x  | 
ph } ) )
4 abid 2444 . . . 4  |-  ( x  e.  { x  | 
ph }  <->  ph )
54bibi2i 313 . . 3  |-  ( ( x  e.  A  <->  x  e.  { x  |  ph }
)  <->  ( x  e.  A  <->  ph ) )
65albii 1641 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  { x  |  ph } )  <->  A. x
( x  e.  A  <->  ph ) )
73, 6bitri 249 1  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1393    = wceq 1395    e. wcel 1819   {cab 2442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452
This theorem is referenced by:  abeq1  2582  abbi2i  2590  abbi2dv  2594  clabel  2603  sbabelOLD  2651  rabid2  3035  ru  3326  sbcabel  3412  dfss2  3488  zfrep4  4576  pwex  4639  dmopab3  5225  funimaexg  5671
  Copyright terms: Public domain W3C validator