NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  abeq2 Unicode version

Theorem abeq2 2458
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 2463 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 (that has a free variable ) to a theorem with a class variable , we substitute for throughout and simplify, where is a new class variable not already in the wff. An example is the conversion of zfauscl in set.mm to inex1 in set.mm (look at the instance of zfauscl that occurs in the proof of inex1 ). Conversely, to convert a theorem with a class variable to one with , we substitute for throughout and simplify, where and are new setvar and wff variables not already in the wff. An example is cp in set.mm , which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 in set.mm. 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
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem abeq2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax-17 1616 . . 3
2 hbab1 2342 . . 3
31, 2cleqh 2450 . 2
4 abid 2341 . . . 4
54bibi2i 304 . . 3
65albii 1566 . 2
73, 6bitri 240 1
Colors of variables: wff setvar class
Syntax hints:   wb 176  wal 1540   wceq 1642   wcel 1710  cab 2339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349
This theorem is referenced by:  abeq1  2459  abbi2i  2464  abbi2dv  2468  clabel  2474  sbabel  2515  rabid2  2788  ru  3045  sbcabel  3123  1cex  4142  ltfinex  4464  eqpwrelk  4478  evenodddisjlem1  4515  nnadjoinlem1  4519  srelk  4524  tfinnnlem1  4533  dmopab3  4917  ovcelem1  6171
  Copyright terms: Public domain W3C validator