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

Theorem abid1 2731
 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 2605. The proof does not rely on cvjust 2605, so cvjust 2605 could be proved as a special instance of it. Note however that abid1 2731 necessarily relies on df-clel 2606, whereas cvjust 2605 does not. This theorem requires ax-ext 2590, df-clab 2597, df-cleq 2603, df-clel 2606, but to prove that any specific class term not containing class variables is a setvar or can be written as (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 1474, cab 2596 and statements corresponding to defined class constructors. Note on the simultaneous presence in set.mm of this abid1 2731 and its commuted form abid2 2732: 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 2632 (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, and a "computational form" where the shorter expression is on the rhs. An example is df-2 10956 versus 1p1e2 11011. We do not need 1p1e2 11011, 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 11029, 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 computationa form is often more natural. The situation is similar with biconditionals in propositional calculus: see for instance pm4.24 673 and anidm 674, 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 2731 and abid2 2732 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 250 . 2 (𝑥𝐴𝑥𝐴)
21abbi2i 2725 1 𝐴 = {𝑥𝑥𝐴}
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∈ wcel 1977  {cab 2596 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606 This theorem is referenced by:  abid2  2732  inrab2  3859  riotaclbgBAD  33258  aomclem4  36645
 Copyright terms: Public domain W3C validator