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

Theorem abeq2 2188
 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 2193 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 1460 . . 3
2 hbab1 2071 . . 3
31, 2cleqh 2179 . 2
4 abid 2070 . . . 4
54bibi2i 225 . . 3
65albii 1400 . 2
73, 6bitri 182 1
 Colors of variables: wff set class Syntax hints:   wb 103  wal 1283   wceq 1285   wcel 1434  cab 2068 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078 This theorem is referenced by:  abeq1  2189  abbi2i  2194  abbi2dv  2198  clabel  2205  sbabel  2245  rabid2  2531  ru  2815  sbcabel  2896  dfss2  2989  pwex  3961  dmopab3  4576
 Copyright terms: Public domain W3C validator