Theorem wl-df.clel

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

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

Alternate characterizations of A e. B when either A or B is a set are given by clel2g , clel3g , and clel4g .

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

Although the class definitions df-clab , df-cleq , and df-clel 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 . (Contributed by NM, 26-May-1993) (Revised by BJ, 27-Jun-2019)

	Ref	Expression
Hypotheses	wl-df.clel.1	$$⊢y\in z\leftrightarrow \exists u\left(u=y\wedge u\in z\right)$$
	wl-df.clel.2	$$⊢t\in t\leftrightarrow \exists v\left(v=t\wedge v\in t\right)$$
Assertion	wl-df.clel	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-df.clel.1	$$⊢y\in z\leftrightarrow \exists u\left(u=y\wedge u\in z\right)$$
2		wl-df.clel.2	$$⊢t\in t\leftrightarrow \exists v\left(v=t\wedge v\in t\right)$$
3	1 2	df-clel	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$