Theorem wl-df.clel 38354

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.

The hypotheses assert that every instance of the conclusion obtained by substituting the class variables with set variables already holds. Thus, this definition extends to class variables a relation already valid for set variables, and is therefore conservative. This only sketches the conservativity arguement; for details see Appendix of [Levy] p. 357. For this reason we regard this statement as a "definition", even though it does not have the usual form of a definition. Under a stricter syntactic criterion, df-clel 2835 would instead be an axiom.

See also comments under df-clab 2739, df-cleq 2752, and eqabb 2899.

Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2g 3612, clel3g 3614, and clel4g 3616.

[Levy] p. 338 refers to this as the "axiom of membership", treating the theory of classes as an extralogical extension to our logic and set theory axioms.

Under this definition, class members can only be sets; classes are therefore collections of sets. Although the extensionality expressed in df-cleq 2752 already points in this direction, an unusual interpretation of equality could still permit proper classes as members.

Although the class definitions df-clab 2739, df-cleq 2752, and df-clel 2835 are eliminable and conservative, and hence meet the requirements for sound definitions, they are technically axioms in that they do not satisfy the syntactic requirements enforced by the current definition checker. The conservativity proofs require external justification beyond the scope of the checker.

For a general discussion of the theory of classes, see mmset.html#class 2835. (Contributed by NM, 26-May-1993.) (Revised by BJ, 27-Jun-2019.)

Hypotheses

Ref	Expression
wl-df.clel.1	⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
wl-df.clel.2	⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))

Assertion

Ref	Expression
wl-df.clel	⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑡,𝑢,𝑣,𝐴   𝑥,𝐵,𝑦,𝑧,𝑡,𝑢,𝑣

Proof of Theorem wl-df.clel

Step	Hyp	Ref	Expression
1		wl-df.clel.1	. 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
2		wl-df.clel.2	. 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))
3	1, 2	df-clel 2835	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145

This proof depends on definitions:  df-clel 2835

This theorem is used by:  wl-dfclel.basic  38355