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

Definition df-clel 2616
 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 2613 it extends or "overloads" the use of the existing membership symbol, but unlike df-cleq 2613 it does not strengthen the set of valid wffs of logic when the class variables are replaced with setvar variables (see cleljust 1996), so we don't include any set theory axiom as a hypothesis. See also comments about the syntax under df-clab 2607. Alternate definitions of 𝐴 ∈ 𝐵 (but that require either 𝐴 or 𝐵 to be a set) are shown by clel2 3333, clel3 3335, and clel4 3336. 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 2607, df-cleq 2613, and df-clel 2616 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 1988 . 2 wff 𝐴𝐵
4 vx . . . . . 6 setvar 𝑥
54cv 1480 . . . . 5 class 𝑥
65, 1wceq 1481 . . . 4 wff 𝑥 = 𝐴
75, 2wcel 1988 . . . 4 wff 𝑥𝐵
86, 7wa 384 . . 3 wff (𝑥 = 𝐴𝑥𝐵)
98, 4wex 1702 . 2 wff 𝑥(𝑥 = 𝐴𝑥𝐵)
103, 9wb 196 1 wff (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  eleq1w  2682  eleq2w  2683  eleq1d  2684  eleq2d  2685  eleq2dALT  2686  clelab  2746  clabel  2747  nfeld  2770  risset  3058  isset  3202  elex  3207  sbcabel  3510  ssel  3589  disjsn  4237  pwpw0  4335  pwsnALT  4420  mptpreima  5616  fi1uzind  13262  brfi1indALT  13265  fi1uzindOLD  13268  brfi1indALTOLD  13271  ballotlem2  30524  eldm3  31627  bj-clabel  32758  eliminable3a  32819  eliminable3b  32820  bj-denotes  32833  bj-issetwt  32834  bj-elissetv  32836  bj-ax8  32862  bj-df-clel  32863  bj-elsngl  32931
 Copyright terms: Public domain W3C validator