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

Theorem abeq2 2191
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 2196 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 2072 . . 3 (𝑦 ∈ {𝑥𝜑} → ∀𝑥 𝑦 ∈ {𝑥𝜑})
31, 2cleqh 2182 . 2 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}))
4 abid 2071 . . . 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 2069
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 2065
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079
This theorem is referenced by:  abeq1  2192  abbi2i  2197  abbi2dv  2201  clabel  2208  sbabel  2248  rabid2  2536  ru  2825  sbcabel  2906  dfss2  2999  pwex  3979  dmopab3  4605
  Copyright terms: Public domain W3C validator