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

Theorem abeq2 2614
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 2619 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 4560 to inex1 4577 (look at the instance of zfauscl 4560 that occurs in the proof of inex1 4577). 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 3697 and cp 8447; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 8446. 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 1789 . . 3 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
2 hbab1 2494 . . 3 (𝑦 ∈ {𝑥𝜑} → ∀𝑥 𝑦 ∈ {𝑥𝜑})
31, 2cleqh 2606 . 2 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}))
4 abid 2493 . . . 4 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
54bibi2i 322 . . 3 ((𝑥𝐴𝑥 ∈ {𝑥𝜑}) ↔ (𝑥𝐴𝜑))
65albii 1720 . 2 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}) ↔ ∀𝑥(𝑥𝐴𝜑))
73, 6bitri 259 1 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 191  wal 1466   = wceq 1468  wcel 1937  {cab 2491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501
This theorem is referenced by:  abeq1  2615  abbi2i  2620  abbi2dv  2624  clabel  2631  rabid2  2989  ru  3290  sbcabel  3369  dfss2  3443  zfrep4  4556  pwex  4624  dmopab3  5096  funimaexg  5715
  Copyright terms: Public domain W3C validator