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 5295 to inex1 5311 (look at the instance of zfauscl 5295 that occurs in the proof of inex1 5311). 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 4247 and cp 9870; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 9869. 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  3773  sbcabel  3869  dfss2OLD  3966  zfrep4  5290  dmopab3  5912  funimaexgOLD  6625  fineqvrep  33990  bj-ru1  35692  bj-abex  35779  sticksstones1  40831  sticksstones2  40832
  Copyright terms: Public domain W3C validator