Theorem eleq1ab

Description: Extension (in the sense of Remark 3 of the comment of df-clab ) of elequ1 from formulas of the form "setvar e. setvar" to formulas of the form "setvar e. class abstraction". This extension does not require ax-8 contrary to elequ1 , but recall from Remark 3 of the comment of df-clab that it can be considered an extension only because of cvjust , which does require ax-8 .

This is an instance of eleq1w where the containing class is a class abstraction, and contrary to it, it can be proved without df-clel . See also eleq1 for general classes.

The straightforward yet important fact that this statement can be proved from FOL= plus df-clab (hence without ax-ext , df-cleq or df-clel ) was stressed by Mario Carneiro. (Contributed by BJ, 17-Aug-2023)

	Ref	Expression
Assertion	eleq1ab	$$⊢x=y\to \left(x\in \left\{z|\phi \right\}\leftrightarrow y\in \left\{z|\phi \right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbequ	$$⊢x=y\to \left(\left[x/z\right]\phi \leftrightarrow \left[y/z\right]\phi \right)$$
2		df-clab	$$⊢x\in \left\{z|\phi \right\}\leftrightarrow \left[x/z\right]\phi$$
3		df-clab	$$⊢y\in \left\{z|\phi \right\}\leftrightarrow \left[y/z\right]\phi$$
4	1 2 3	3bitr4g	$$⊢x=y\to \left(x\in \left\{z|\phi \right\}\leftrightarrow y\in \left\{z|\phi \right\}\right)$$