Theorem wl-dfcleq.basic

Description: This theorem is a conservative extension of ax-ext to classes, with no hypotheses. It is not complete, since ax-8 can be derived (see in-ax8 ) via alpha-renaming.

Although not suitable for general use, it suffices for the development of the following types of theorems, which are not affected by alpha-renaming:

1. Theorems with no bound variables in the hypotheses or conclusion (see eqriv ).

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

3. Theorems with distinct bound variables arising only through implicit substitution (see eqabbw ).

Remark: the proof uses axextb to prove the hypothesis of df-cleq that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen , equid }. (Contributed by NM, 15-Sep-1993) (Revised by BJ, 24-Jun-2019)

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

Proof

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