Definition df-clel 1449

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

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 1105	. 2 wff A e. B
4		vx	. . . . . 6 set x
5	4	cv 1098	. . . . 5 class x
6	5, 1	wceq 1099	. . . 4 wff x = A
7	5, 2	wcel 1105	. . . 4 wff x e. B
8	6, 7	wa 223	. . 3 wff (x = A /\ x e. B)
9	8, 4	wex 956	. 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 1510  eleq2 1511  hbel 1542  clelab 1557  clabel 1558  sbabel 1560  risset 1661  isset 1789  elisset 1792  sbcabel 1967  sbcel12g 1982  ssel 2034  pwpw0 2439  opelxp 3176  prnmadd 5023

Copyright terms: Public domain