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

Theorem eqabb 2873
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 abbib 2804 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 5301 to inex1 5317 (look at the instance of zfauscl 5301 that occurs in the proof of inex1 5317). 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 4250 and cp 9888; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 9887. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13.

Usage of eqabbw 2809 is preferred since it requires fewer axioms. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2025.)

Assertion
Ref Expression
eqabb (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eqabb
StepHypRef Expression
1 abid1 2870 . . 3 𝐴 = {𝑥𝑥𝐴}
21eqeq1i 2737 . 2 (𝐴 = {𝑥𝜑} ↔ {𝑥𝑥𝐴} = {𝑥𝜑})
3 abbib 2804 . 2 ({𝑥𝑥𝐴} = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
42, 3bitri 274 1 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wal 1539   = wceq 1541  wcel 2106  {cab 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810
This theorem is referenced by:  eqabcb  2875  clabel  2881  rabid2OLD  3465  ru  3776  sbcabel  3872  dfss2OLD  3969  zfrep4  5296  dmopab3  5919  funimaexgOLD  6635  fineqvrep  34381  bj-ru1  36127  bj-abex  36214  sticksstones1  41268  sticksstones2  41269
  Copyright terms: Public domain W3C validator