Theorem wl-df.clel 37874

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 2815 would instead be an axiom.

See also comments under df-clab 2719, df-cleq 2732, and eqabb 2879.

Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2g 3604, clel3g 3606, and clel4g 3608.

[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 2732 already points in this direction, an unusual interpretation of equality could still permit proper classes as members.

Although the class definitions df-clab 2719, df-cleq 2732, and df-clel 2815 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 2815. (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 2815	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119

This theorem depends on definitions:  df-clel 2815

This theorem is referenced by:  wl-dfclel.basic  37875