Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  abeq2 Unicode version

Theorem abeq2 2249
 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 2254 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. Conversely, to convert a theorem with a class variable to one with , we substitute for throughout and simplify, where and are new set and wff variables not already in the wff. 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 1507 . . 3
2 hbab1 2129 . . 3
31, 2cleqh 2240 . 2
4 abid 2128 . . . 4
54bibi2i 226 . . 3
65albii 1447 . 2
73, 6bitri 183 1
 Colors of variables: wff set class Syntax hints:   wb 104  wal 1330   wceq 1332   wcel 1481  cab 2126 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136 This theorem is referenced by:  abeq1  2250  abbi2i  2255  abbi2dv  2259  clabel  2267  sbabel  2308  rabid2  2610  ru  2912  sbcabel  2994  dfss2  3091  vpwex  4111  dmopab3  4760
 Copyright terms: Public domain W3C validator