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

Theorem abeq2 2761
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 2766 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 4816 to inex1 4832 (look at the instance of zfauscl 4816 that occurs in the proof of inex1 4832). 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 3884 and cp 8792; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 8791. 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 1879 . . 3 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
2 hbab1 2640 . . 3 (𝑦 ∈ {𝑥𝜑} → ∀𝑥 𝑦 ∈ {𝑥𝜑})
31, 2cleqh 2753 . 2 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}))
4 abid 2639 . . . 4 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
54bibi2i 326 . . 3 ((𝑥𝐴𝑥 ∈ {𝑥𝜑}) ↔ (𝑥𝐴𝜑))
65albii 1787 . 2 (∀𝑥(𝑥𝐴𝑥 ∈ {𝑥𝜑}) ↔ ∀𝑥(𝑥𝐴𝜑))
73, 6bitri 264 1 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1521   = wceq 1523  wcel 2030  {cab 2637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647
This theorem is referenced by:  abeq1  2762  abbi2i  2767  abbi2dv  2771  clabel  2778  rabid2  3148  ru  3467  sbcabel  3550  dfss2  3624  zfrep4  4812  pwex  4878  dmopab3  5369  funimaexg  6013
  Copyright terms: Public domain W3C validator