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

Definition df-clel 2606
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 2603 it extends or "overloads" the use of the existing membership symbol, but unlike df-cleq 2603 it does not strengthen the set of valid wffs of logic when the class variables are replaced with setvar variables (see cleljust 1985), so we don't include any set theory axiom as a hypothesis. See also comments about the syntax under df-clab 2597. Alternate definitions of 𝐴𝐵 (but that require either 𝐴 or 𝐵 to be a set) are shown by clel2 3309, clel3 3311, and clel4 3312.

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 2597, df-cleq 2603, and df-clel 2606 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 1977 . 2 wff 𝐴𝐵
4 vx . . . . . 6 setvar 𝑥
54cv 1474 . . . . 5 class 𝑥
65, 1wceq 1475 . . . 4 wff 𝑥 = 𝐴
75, 2wcel 1977 . . . 4 wff 𝑥𝐵
86, 7wa 383 . . 3 wff (𝑥 = 𝐴𝑥𝐵)
98, 4wex 1695 . 2 wff 𝑥(𝑥 = 𝐴𝑥𝐵)
103, 9wb 195 1 wff (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  eleq1d  2672  eleq2d  2673  eleq2dOLD  2674  eleq2dALT  2675  clelab  2735  clabel  2736  nfeld  2759  risset  3044  isset  3180  elex  3185  sbcabel  3483  ssel  3562  disjsn  4192  pwpw0  4284  pwsnALT  4367  mptpreima  5545  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  ballotlem2  29877  eldm3  30905  bj-clabel  31971  eliminable3a  32037  eliminable3b  32038  bj-eleq1w  32040  bj-eleq2w  32041  bj-denotes  32052  bj-issetwt  32053  bj-elissetv  32055  bj-ax8  32080  bj-df-clel  32081  bj-elsngl  32149
  Copyright terms: Public domain W3C validator