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

Theorem abeq2 2128
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 2133 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 1400 . . 3 (y Ax y A)
2 hbab1 2011 . . 3 (y {xφ} → x y {xφ})
31, 2cleqh 2119 . 2 (A = {xφ} ↔ x(x Ax {xφ}))
4 abid 2010 . . . 4 (x {xφ} ↔ φ)
54bibi2i 216 . . 3 ((x Ax {xφ}) ↔ (x Aφ))
65albii 1339 . 2 (x(x Ax {xφ}) ↔ x(x Aφ))
73, 6bitri 173 1 (A = {xφ} ↔ x(x Aφ))
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1226   = wceq 1228   wcel 1374  {cab 2008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018
This theorem is referenced by:  abeq1  2129  abbi2i  2134  abbi2dv  2138  clabel  2145  sbabel  2185  rabid2  2462  ru  2738  sbcabel  2814  dfss2  2909  pwex  3904  dmopab3  4473
  Copyright terms: Public domain W3C validator