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

Theorem eqabb 2878
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 2808 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 5303 to inex1 5322 (look at the instance of zfauscl 5303 that occurs in the proof of inex1 5322). 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 4266 and cp 9928; the latter derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 9927. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13.

Usage of eqabbw 2812 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 2875 . . 3 𝐴 = {𝑥𝑥𝐴}
21eqeq1i 2739 . 2 (𝐴 = {𝑥𝜑} ↔ {𝑥𝑥𝐴} = {𝑥𝜑})
3 abbib 2808 . 2 ({𝑥𝑥𝐴} = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
42, 3bitri 275 1 (𝐴 = {𝑥𝜑} ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wal 1534   = wceq 1536  wcel 2105  {cab 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813
This theorem is referenced by:  eqabcb  2880  clabel  2885  rabid2OLD  3468  ruOLD  3789  sbcabel  3886  zfrep4  5298  dmopab3  5932  rnopab3  5969  funimaexgOLD  6654  fineqvrep  35087  bj-abex  37012  sticksstones1  42127  sticksstones2  42128
  Copyright terms: Public domain W3C validator