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

Theorem abeq2 2050
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 2055 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 x) to a theorem with a class variable A, we substitute x A for φ throughout and simplify, where A is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable A to one with φ, we substitute {xφ} for A throughout and simplify, where x 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 (A = {xφ} ↔ x(x Aφ))
Distinct variable group:   x,A
Allowed substitution hint:   φ(x)

Proof of Theorem abeq2
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 ax-17 1367 . . 3 (y Ax y A)
2 hbab1 1934 . . 3 (y {xφ} → x y {xφ})
31, 2cleqh 2042 . 2 (A = {xφ} ↔ x(x Ax {xφ}))
4 abid 1933 . . . 4 (x {xφ} ↔ φ)
54bibi2i 214 . . 3 ((x Ax {xφ}) ↔ (x Aφ))
65albii 1305 . 2 (x(x Ax {xφ}) ↔ x(x Aφ))
73, 6bitri 171 1 (A = {xφ} ↔ x(x Aφ))
Colors of variables: wff set class
Syntax hints:  wb 96  wal 1281   = wceq 1340   wcel 1342  {cab 1931
This theorem is referenced by:  abeq1  2051  abbi2i  2056  abbi2dv  2060  clabel  2066  sbabel  2106  rabid2  2370  ru  2643  sbcabel  2720  dfss2  2819
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-5 1282  ax-7 1283  ax-gen 1284  ax-ie1 1329  ax-ie2 1330  ax-8 1344  ax-11 1346  ax-4 1349  ax-17 1367  ax-i9 1371  ax-ial 1376  ax-i5r 1377  ax-ext 1928
This theorem depends on definitions:  df-bi 108  df-nf 1296  df-sb 1586  df-clab 1932  df-cleq 1938  df-clel 1941
  Copyright terms: Public domain W3C validator