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

Definition df-clel 2773
 Description: Define the membership connective between classes. Theorem 6.3 of [Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we adopt as a definition. See these references for its metalogical justification. Note that like df-cleq 2769 it extends or "overloads" the use of the existing membership symbol, but unlike df-cleq 2769 it does not strengthen the set of valid wffs of logic when the class variables are replaced with setvar variables (see cleljust 2114), so we don't include any set theory axiom as a hypothesis. See also comments about the syntax under df-clab 2763. Alternate definitions of 𝐴 ∈ 𝐵 (but that require either 𝐴 or 𝐵 to be a set) are shown by clel2 3542, clel3 3544, and clel4 3545. This is called the "axiom of membership" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. While the three class definitions df-clab 2763, df-cleq 2769, and df-clel 2773 are eliminable and conservative and thus meet the requirements for sound definitions, they are technically axioms in that they do not satisfy the requirements for the current definition checker. The proofs of conservativity require external justification that is beyond the scope of the definition checker. For a general discussion of the theory of classes, see mmset.html#class. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
df-clel (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Detailed syntax breakdown of Definition df-clel
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wcel 2106 . 2 wff 𝐴𝐵
4 vx . . . . . 6 setvar 𝑥
54cv 1600 . . . . 5 class 𝑥
65, 1wceq 1601 . . . 4 wff 𝑥 = 𝐴
75, 2wcel 2106 . . . 4 wff 𝑥𝐵
86, 7wa 386 . . 3 wff (𝑥 = 𝐴𝑥𝐵)
98, 4wex 1823 . 2 wff 𝑥(𝑥 = 𝐴𝑥𝐵)
103, 9wb 198 1 wff (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  eleq1w  2841  eleq2w  2842  eleq1d  2843  eleq2d  2844  eleq2dALT  2845  clelab  2915  clabel  2916  nfeld  2942  risset  3246  isset  3408  elex  3413  sbcabel  3733  ssel  3814  noel  4145  disjsn  4477  pwpw0  4575  pwsnALT  4664  mptpreima  5882  fi1uzind  13593  brfi1indALT  13596  ballotlem2  31149  eldm3  32245  bj-clabel  33360  eliminable3a  33419  eliminable3b  33420  bj-denotes  33427  bj-issetwt  33429  bj-elissetv  33431  bj-ax8  33458  bj-df-clel  33459  bj-elsngl  33528
 Copyright terms: Public domain W3C validator