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

Theorem abeq2 2146
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 2151 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 1419 . . 3 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
2 hbab1 2029 . . 3 (𝑦 ∈ {𝑥𝜑} → ∀𝑥 𝑦 ∈ {𝑥𝜑})
31, 2cleqh 2137 . 2 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}))
4 abid 2028 . . . 4 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
54bibi2i 216 . . 3 ((𝑥𝐴𝑥 ∈ {𝑥𝜑}) ↔ (𝑥𝐴𝜑))
65albii 1359 . 2 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}) ↔ ∀𝑥(𝑥𝐴𝜑))
73, 6bitri 173 1 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1241   = wceq 1243  wcel 1393  {cab 2026
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 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036
This theorem is referenced by:  abeq1  2147  abbi2i  2152  abbi2dv  2156  clabel  2163  sbabel  2203  rabid2  2486  ru  2763  sbcabel  2839  dfss2  2934  pwex  3932  dmopab3  4548
  Copyright terms: Public domain W3C validator