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

Theorem abeq2 2388
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 2393 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 4143 to inex1 4155 (look at the instance of zfauscl 4143 that occurs in the proof of inex1 4155). 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 7561, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 7560. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-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-17 1603 . . 3  |-  ( y  e.  A  ->  A. x  y  e.  A )
2 hbab1 2272 . . 3  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2cleqh 2380 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  x  e.  { x  | 
ph } ) )
4 abid 2271 . . . 4  |-  ( x  e.  { x  | 
ph }  <->  ph )
54bibi2i 304 . . 3  |-  ( ( x  e.  A  <->  x  e.  { x  |  ph }
)  <->  ( x  e.  A  <->  ph ) )
65albii 1553 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  { x  |  ph } )  <->  A. x
( x  e.  A  <->  ph ) )
73, 6bitri 240 1  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527    = wceq 1623    e. wcel 1684   {cab 2269
This theorem is referenced by:  abeq1  2389  abbi2i  2394  abbi2dv  2398  clabel  2404  sbabel  2445  rabid2  2717  ru  2990  sbcabel  3068  dfss2  3169  zfrep4  4139  pwex  4193  dmopab3  4891  funimaexg  5329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator