ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-clel Structured version   Unicode version

Definition df-clel 2009
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 2006 it extends or "overloads" the use of the existing membership symbol, but unlike df-cleq 2006 it does not strengthen the set of valid wffs of logic when the class variables are replaced with setvar variables (see cleljust 1786), so we don't include any set theory axiom as a hypothesis. See also comments about the syntax under df-clab 2000.

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.

For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (Contributed by NM, 5-Aug-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 1366 . 2
4 vx . . . . . 6  setvar
54cv 1222 . . . . 5
65, 1wceq 1223 . . . 4
75, 2wcel 1366 . . . 4
86, 7wa 97 . . 3
98, 4wex 1354 . 2
103, 9wb 98 1
Colors of variables: wff set class
This definition is referenced by:  eleq1  2073  eleq2  2074  clelab  2135  clabel  2136  nfel  2159  nfeld  2166  sbabel  2176  risset  2321  isset  2530  elex  2534  sbcabel  2807  ssel  2907  disjsn  3395  mptpreima  4729
  Copyright terms: Public domain W3C validator