Definition df-clel 1099

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

Assertion

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

Distinct variable group(s):   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 1092	. 2 wff A ∈ B
4		vx	. . . . . 6 set x
5	4	cv 1089	. . . . 5 class x
6	5, 1	wceq 1091	. . . 4 wff x = A
7	5, 2	wcel 1092	. . . 4 wff x ∈ B
8	6, 7	wa 196	. . 3 wff (x = A ∧ x ∈ B)
9	8, 4	wex 678	. 2 wff ∃x(x = A ∧ x ∈ B)
10	3, 9	wb 127	1 wff (A ∈ B ↔ ∃x(x = A ∧ x ∈ B))

This definition is referenced by:  eleq1 1149  eleq2 1150  hbel 1172  clelab 1187  sbabel 1189  risset 1235  isset 1351  elisset 1354  ssel 1502  pwpw0 1883  opelxp 2452  prnmadd 3894

metamath.org