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 -> ( x e. { z | ph } <-> y e. { z | ph } ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ	|- ( x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) )
2		df-clab	|- ( x e. { z | ph } <-> [ x / z ] ph )
3		df-clab	|- ( y e. { z | ph } <-> [ y / z ] ph )
4	1 2 3	3bitr4g	|- ( x = y -> ( x e. { z | ph } <-> y e. { z | ph } ) )