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

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

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 2443, df-cleq 2449, and df-clel 2452 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 http://us.metamath.org/mpeuni/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
2 cB . . 3
31, 2wcel 1818 . 2
4 vx . . . . . 6
54cv 1394 . . . . 5
65, 1wceq 1395 . . . 4
75, 2wcel 1818 . . . 4
86, 7wa 369 . . 3
98, 4wex 1612 . 2
103, 9wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  eleq1d  2526  eleq2d  2527  eleq2dALT  2528  eleq1OLD  2531  eleq2OLD  2532  clelab  2601  clelabOLD  2602  clabel  2603  nfeld  2627  nfelOLD  2633  sbabelOLD  2651  risset  2982  isset  3113  elex  3118  sbcabel  3416  ssel  3497  disjsn  4090  pwpw0  4178  pwsnALT  4244  mptpreima  5505  brfi1uzind  12532  ballotlem2  28427  eldm3  29191  bj-clabel  34369  eliminable3a  34419  eliminable3b  34420  bj-eleq1w  34422  bj-eleq2w  34423  bj-denotes  34434  bj-issetwt  34435  bj-elissetv  34437  bj-df-clel  34462  bj-elsngl  34526
  Copyright terms: Public domain W3C validator