Theorem wl-df.clel 37953

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

See also comments under df-clab 2735, df-cleq 2748, and eqabb 2895.

Alternate characterizations of 𝐴 ∈ 𝐵 when either 𝐴 or 𝐵 is a set are given by clel2g 3613, clel3g 3615, and clel4g 3617.

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

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1554  ∃wex 1793   ∈ wcel 2136

This theorem depends on definitions:  df-clel 2831

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