Definition df-clel 1475

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

Assertion

Ref	Expression
df-clel	|- (A e. B <-> E.x(x = A /\ x e. 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 960	. 2 wff A e. B
4		vx	. . . . . 6 set x
5	4	cv 957	. . . . 5 class x
6	5, 1	wceq 958	. . . 4 wff x = A
7	5, 2	wcel 960	. . . 4 wff x e. B
8	6, 7	wa 223	. . 3 wff (x = A /\ x e. B)
9	8, 4	wex 982	. 2 wff E.x(x = A /\ x e. B)
10	3, 9	wb 146	1 wff (A e. B <-> E.x(x = A /\ x e. B))

This definition is referenced by:  eleq1 1537  eleq2 1538  hbel 1569  clelab 1584  clabel 1585  sbabel 1587  risset 1688  isset 1817  elisset 1820  sbcabel 2000  sbcel12g 2015  ssel 2067  pwpw0 2474  pwsnALT 2506  opelxp 3221  prnmadd 5119

Copyright terms: Public domain