Definition df-clel 1514

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

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 994	. 2 wff A ∈ B
4		vx	. . . . . 6 set x
5	4	cv 991	. . . . 5 class x
6	5, 1	wceq 992	. . . 4 wff x = A
7	5, 2	wcel 994	. . . 4 wff x ∈ B
8	6, 7	wa 221	. . 3 wff (x = A ⋀ x ∈ B)
9	8, 4	wex 1016	. 2 wff ∃x(x = A ⋀ x ∈ B)
10	3, 9	wb 144	1 wff (A ∈ B ↔ ∃x(x = A ⋀ x ∈ B))

This definition is referenced by:  eleq1 1577  eleq2 1578  hbel 1609  clelab 1624  clabel 1625  sbabel 1627  risset 1731  isset 1860  elisset 1863  sbc8g 2004  sbcabel 2046  sbcel12g 2062  ssel 2115  pwpw0 2533  pwsnALT 2566  opelxp 3297  prnmadd 5254

Copyright terms: Public domain