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

Theorem abid1 2871
Description: Every class is equal to a class abstraction (the class of sets belonging to it). Theorem 5.2 of [Quine] p. 35. This is a generalization to classes of cvjust 2727. The proof does not rely on cvjust 2727, so cvjust 2727 could be proved as a special instance of it. Note however that abid1 2871 necessarily relies on df-clel 2811, whereas cvjust 2727 does not.

This theorem requires ax-ext 2704, df-clab 2711, df-cleq 2725, df-clel 2811, but to prove that any specific class term not containing class variables is a setvar or is equal to a class abstraction does not require these $a-statements. This last fact is a metatheorem, consequence of the fact that the only $a-statements with typecode class are cv 1541, cab 2710, and statements corresponding to defined class constructors.

Note on the simultaneous presence in set.mm of this abid1 2871 and its commuted form abid2 2872: It is rare that two forms so closely related both appear in set.mm. Indeed, such equalities are generally used in later proofs as parts of transitive inferences, and with the many variants of eqtri 2761 (search for *eqtr*), it would be rare that either one would shorten a proof compared to the other. There is typically a choice between what we call a "definitional form", where the shorter expression is on the LHS (left-hand side), and a "computational form", where the shorter expression is on the RHS (right-hand side). An example is df-2 12224 versus 1p1e2 12286. We do not need 1p1e2 12286, but because it occurs "naturally" in computations, it can be useful to have it directly, together with a uniform set of 1-digit operations like 1p2e3 12304, etc. In most cases, we do not need both a definitional and a computational forms. A definitional form would favor consistency with genuine definitions, while a computational form is often more natural. The situation is similar with biconditionals in propositional calculus: see for instance pm4.24 565 and anidm 566, while other biconditionals generally appear in a single form (either definitional, but more often computational). In the present case, the equality is important enough that both abid1 2871 and abid2 2872 are in set.mm.

(Contributed by NM, 26-Dec-1993.) (Revised by BJ, 10-Nov-2020.)

Assertion
Ref Expression
abid1 𝐴 = {𝑥𝑥𝐴}
Distinct variable group:   𝑥,𝐴

Proof of Theorem abid1
StepHypRef Expression
1 biid 261 . 2 (𝑥𝐴𝑥𝐴)
21abbi2i 2870 1 𝐴 = {𝑥𝑥𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  {cab 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811
This theorem is referenced by:  abid2  2872  eqabr  2873  eqab  2874  abssdv  4029  inrab2  4271  nsgqusf1olem2  32247  disjdmqscossss  37315  riotaclbgBAD  37466  ssabdv  40692  aomclem4  41431  limexissupab  41665
  Copyright terms: Public domain W3C validator