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

Theorem abeq2 2571
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 2576 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 4541 to inex1 4558 (look at the instance of zfauscl 4541 that occurs in the proof of inex1 4558). 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 3682 and cp 8388; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 8387. 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 1769 . . 3  |-  ( y  e.  A  ->  A. x  y  e.  A )
2 hbab1 2451 . . 3  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2cleqh 2563 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  x  e.  { x  | 
ph } ) )
4 abid 2450 . . . 4  |-  ( x  e.  { x  | 
ph }  <->  ph )
54bibi2i 319 . . 3  |-  ( ( x  e.  A  <->  x  e.  { x  |  ph }
)  <->  ( x  e.  A  <->  ph ) )
65albii 1702 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  { x  |  ph } )  <->  A. x
( x  e.  A  <->  ph ) )
73, 6bitri 257 1  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   A.wal 1453    = wceq 1455    e. wcel 1898   {cab 2448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458
This theorem is referenced by:  abeq1  2572  abbi2i  2577  abbi2dv  2581  clabel  2588  sbabelOLD  2632  rabid2  2980  ru  3278  sbcabel  3357  dfss2  3433  zfrep4  4537  pwex  4600  dmopab3  5066  funimaexg  5682
  Copyright terms: Public domain W3C validator