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

Theorem abeq2 2391
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 2396 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 4146 to inex1 4158 (look at the instance of zfauscl 4146 that occurs in the proof of inex1 4158). 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 7558, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 7557. 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
Dummy variable  y is distinct from all other variables.
Allowed substitution group:    ph( x)

Proof of Theorem abeq2
StepHypRef Expression
1 ax-17 1605 . . 3  |-  ( y  e.  A  ->  A. x  y  e.  A )
2 hbab1 2275 . . 3  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2cleqh 2383 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  x  e.  { x  | 
ph } ) )
4 abid 2274 . . . 4  |-  ( x  e.  { x  | 
ph }  <->  ph )
54bibi2i 306 . . 3  |-  ( ( x  e.  A  <->  x  e.  { x  |  ph }
)  <->  ( x  e.  A  <->  ph ) )
65albii 1555 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  { x  |  ph } )  <->  A. x
( x  e.  A  <->  ph ) )
73, 6bitri 242 1  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1529    = wceq 1625    e. wcel 1687   {cab 2272
This theorem is referenced by:  abeq1  2392  abbi2i  2397  abbi2dv  2401  clabel  2407  sbabel  2448  rabid2  2720  ru  2993  sbcabel  3071  dfss2  3172  zfrep4  4142  pwex  4194  dmopab3  4892  funimaexg  5296
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-clab 2273  df-cleq 2279  df-clel 2282
  Copyright terms: Public domain W3C validator