 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  abeq2 Structured version   Visualization version   GIF version

Theorem abeq2 2623
 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 2628 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. An example is the conversion of zfauscl 4609 to inex1 4626 (look at the instance of zfauscl 4609 that occurs in the proof of inex1 4626). Conversely, to convert a theorem with a class variable 𝐴 to one with 𝜑, we substitute {𝑥 ∣ 𝜑} for 𝐴 throughout and simplify, where 𝑥 and 𝜑 are new setvar and wff variables not already in the wff. Examples include dfsymdif2 3716 and cp 8512; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 8511. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 26-May-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-5 1793 . . 3 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
2 hbab1 2503 . . 3 (𝑦 ∈ {𝑥𝜑} → ∀𝑥 𝑦 ∈ {𝑥𝜑})
31, 2cleqh 2615 . 2 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}))
4 abid 2502 . . . 4 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
54bibi2i 325 . . 3 ((𝑥𝐴𝑥 ∈ {𝑥𝜑}) ↔ (𝑥𝐴𝜑))
65albii 1722 . 2 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}) ↔ ∀𝑥(𝑥𝐴𝜑))
73, 6bitri 262 1 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 194  ∀wal 1472   = wceq 1474   ∈ wcel 1938  {cab 2500 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494 This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510 This theorem is referenced by:  abeq1  2624  abbi2i  2629  abbi2dv  2633  clabel  2640  rabid2  3000  ru  3305  sbcabel  3387  dfss2  3461  zfrep4  4605  pwex  4673  dmopab3  5150  funimaexg  5774
 Copyright terms: Public domain W3C validator