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

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 2608, df-cleq 2614, and df-clel 2617 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 1987 . 2 wff 𝐴𝐵
4 vx . . . . . 6 setvar 𝑥
54cv 1479 . . . . 5 class 𝑥
65, 1wceq 1480 . . . 4 wff 𝑥 = 𝐴
75, 2wcel 1987 . . . 4 wff 𝑥𝐵
86, 7wa 384 . . 3 wff (𝑥 = 𝐴𝑥𝐵)
98, 4wex 1701 . 2 wff 𝑥(𝑥 = 𝐴𝑥𝐵)
103, 9wb 196 1 wff (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  eleq1d  2683  eleq2d  2684  eleq2dALT  2685  clelab  2745  clabel  2746  nfeld  2769  risset  3055  isset  3193  elex  3198  sbcabel  3498  ssel  3577  disjsn  4216  pwpw0  4312  pwsnALT  4397  mptpreima  5587  fi1uzind  13218  brfi1indALT  13221  fi1uzindOLD  13224  brfi1indALTOLD  13227  ballotlem2  30328  eldm3  31357  bj-clabel  32423  eliminable3a  32486  eliminable3b  32487  bj-eleq1w  32490  bj-eleq2w  32491  bj-denotes  32502  bj-issetwt  32503  bj-elissetv  32505  bj-ax8  32531  bj-df-clel  32532  bj-elsngl  32600
  Copyright terms: Public domain W3C validator