Theorem wl-dfclel.basic

Description: This theorem gives a conservative extension of membership of classes, without hypotheses. Conservativity alone, however, is insufficient, since issues involving alpha-renaming can still arise, see in-ax8 .

Although unsuitable for general use, it is adequate for the development of theorems unaffected by alpha-renaming, including:

1. Theorems whose hypotheses and conclusion contain no bound variables (see eleq1w ).

2. Theorems using the same bound variable throughout (see elex2 ).

3. Theorems in which distinct bound variables arise only through implicit substitution (see eqabbw ).

(Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	wl-dfclel.basic	$$⊢A\in B\leftrightarrow \exists x\left(x=A\wedge x\in B\right)$$

Proof

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