Theorem cleljustab

Description: Extension of cleljust from formulas of the form "setvar e. setvar" to formulas of the form "setvar e. class abstraction". This is an instance of dfclel where the containing class is a class abstraction. The same remarks as for eleq1ab apply. (Contributed by BJ, 8-Nov-2021) (Proof shortened by Steven Nguyen, 19-May-2023)

	Ref	Expression
Assertion	cleljustab	|- ( x e. { y | ph } <-> E. z ( z = x /\ z e. { y | ph } ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1ab	|- ( z = x -> ( z e. { y | ph } <-> x e. { y | ph } ) )
2	1	equsexvw	|- ( E. z ( z = x /\ z e. { y | ph } ) <-> x e. { y | ph } )
3	2	bicomi	|- ( x e. { y | ph } <-> E. z ( z = x /\ z e. { y | ph } ) )