Definition df-clel 1470

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

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 956	. 2 wff A ∈ B
4		vx	. . . . . 6 set x
5	4	cv 953	. . . . 5 class x
6	5, 1	wceq 954	. . . 4 wff x = A
7	5, 2	wcel 956	. . . 4 wff x ∈ B
8	6, 7	wa 223	. . 3 wff (x = A ⋀ x ∈ B)
9	8, 4	wex 978	. 2 wff ∃x(x = A ⋀ x ∈ B)
10	3, 9	wb 146	1 wff (A ∈ B ↔ ∃x(x = A ⋀ x ∈ B))

This definition is referenced by:  eleq1 1531  eleq2 1532  hbel 1563  clelab 1578  clabel 1579  sbabel 1581  risset 1682  isset 1810  elisset 1813  sbcabel 1992  sbcel12g 2007  ssel 2059  pwpw0 2466  opelxp 3214  prnmadd 5092

Copyright terms: Public domain