Definition df-clel 2349

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

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 https://us.metamath.org/mpeuni/mmset.html#class 2979. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-clel	⊢ (A ∈ B ↔ ∃x(x = A ∧ x ∈ B))

Distinct variable groups:   x,A   x,B

Detailed syntax breakdown of Definition df-clel

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wcel 1710	. 2 wff A ∈ B
4		vx	. . . . . 6 setvar x
5	4	cv 1641	. . . . 5 class x
6	5, 1	wceq 1642	. . . 4 wff x = A
7	5, 2	wcel 1710	. . . 4 wff x ∈ B
8	6, 7	wa 358	. . 3 wff (x = A ∧ x ∈ B)
9	8, 4	wex 1541	. 2 wff ∃x(x = A ∧ x ∈ B)
10	3, 9	wb 176	1 wff (A ∈ B ↔ ∃x(x = A ∧ x ∈ B))

This definition is referenced by:  eleq1  2413  eleq2  2414  clelab  2474  clabel  2475  nfel  2498  nfeld  2505  sbabel  2516  risset  2662  isset  2864  elex  2868  sbcabel  3124  ssel  3268  disjsn  3787  pwpw0  3856  pwsnALT  3883  axcnvprim  4092  axssetprim  4093  axsiprim  4094  axtyplowerprim  4095  axins2prim  4096  axins3prim  4097  dfnnc2  4396  nnsucelrlem1  4425  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  tfinnnlem1  4534  opelxp  4812  mptpreima  5683  composeex  5821  domfnex  5871  ranfnex  5872  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  ceexlem1  6174  tcfnex  6245  nchoicelem11  6300  nchoicelem16  6305