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

Theorem abeq2 2537
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 2542 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 4491 to inex1 4508 (look at the instance of zfauscl 4491 that occurs in the proof of inex1 4508). 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 3643 and cp 8314; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 8313. 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 1752 . . 3  |-  ( y  e.  A  ->  A. x  y  e.  A )
2 hbab1 2417 . . 3  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2cleqh 2529 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  x  e.  { x  | 
ph } ) )
4 abid 2416 . . . 4  |-  ( x  e.  { x  | 
ph }  <->  ph )
54bibi2i 314 . . 3  |-  ( ( x  e.  A  <->  x  e.  { x  |  ph }
)  <->  ( x  e.  A  <->  ph ) )
65albii 1685 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  { x  |  ph } )  <->  A. x
( x  e.  A  <->  ph ) )
73, 6bitri 252 1  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   A.wal 1435    = wceq 1437    e. wcel 1872   {cab 2414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424
This theorem is referenced by:  abeq1  2538  abbi2i  2543  abbi2dv  2547  clabel  2554  sbabelOLD  2598  rabid2  2945  ru  3241  sbcabel  3320  dfss2  3396  zfrep4  4487  pwex  4550  dmopab3  5009  funimaexg  5621
  Copyright terms: Public domain W3C validator