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

Theorem abeq2 2541
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 2546 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 4332 to inex1 4344 (look at the instance of zfauscl 4332 that occurs in the proof of inex1 4344). 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 7815, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 7814. 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 1626 . . 3  |-  ( y  e.  A  ->  A. x  y  e.  A )
2 hbab1 2425 . . 3  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
31, 2cleqh 2533 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  x  e.  { x  | 
ph } ) )
4 abid 2424 . . . 4  |-  ( x  e.  { x  | 
ph }  <->  ph )
54bibi2i 305 . . 3  |-  ( ( x  e.  A  <->  x  e.  { x  |  ph }
)  <->  ( x  e.  A  <->  ph ) )
65albii 1575 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  { x  |  ph } )  <->  A. x
( x  e.  A  <->  ph ) )
73, 6bitri 241 1  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549    = wceq 1652    e. wcel 1725   {cab 2422
This theorem is referenced by:  abeq1  2542  abbi2i  2547  abbi2dv  2551  clabel  2557  sbabel  2598  rabid2  2885  ru  3160  sbcabel  3238  dfss2  3337  zfrep4  4328  pwex  4382  dmopab3  5082  funimaexg  5530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator