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

Definition df-clel 2501
 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 2498 it extends or "overloads" the use of the existing membership symbol, but unlike df-cleq 2498 it does not strengthen the set of valid wffs of logic when the class variables are replaced with setvar variables (see cleljust 1945), so we don't include any set theory axiom as a hypothesis. See also comments about the syntax under df-clab 2492. Alternate definitions of 𝐴 ∈ 𝐵 (but that require either 𝐴 or 𝐵 to be a set) are shown by clel2 3198, clel3 3200, and clel4 3201. 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 2492, df-cleq 2498, and df-clel 2501 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 1937 . 2 wff 𝐴𝐵
4 vx . . . . . 6 setvar 𝑥
54cv 1467 . . . . 5 class 𝑥
65, 1wceq 1468 . . . 4 wff 𝑥 = 𝐴
75, 2wcel 1937 . . . 4 wff 𝑥𝐵
86, 7wa 378 . . 3 wff (𝑥 = 𝐴𝑥𝐵)
98, 4wex 1692 . 2 wff 𝑥(𝑥 = 𝐴𝑥𝐵)
103, 9wb 191 1 wff (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  eleq1d  2567  eleq2d  2568  eleq2dOLD  2569  eleq2dALT  2570  clelab  2630  clabel  2631  nfeld  2654  risset  2937  isset  3070  elex  3075  sbcabel  3369  ssel  3448  disjsn  4060  pwpw0  4149  pwsnALT  4223  mptpreima  5379  fi1uzind  12773  brfi1indALT  12776  fi1uzindOLD  12779  brfi1indALTOLD  12782  ballotlem2  29475  eldm3  30553  bj-clabel  31580  eliminable3a  31636  eliminable3b  31637  bj-eleq1w  31639  bj-eleq2w  31640  bj-denotes  31651  bj-issetwt  31652  bj-elissetv  31654  bj-ax8  31679  bj-df-clel  31680  bj-elsngl  31748
 Copyright terms: Public domain W3C validator