Theorem iseqsetv-clel

Description: Alternate proof of iseqsetv-cleq . The expression E. x x = A does not depend on a particular choice of the set variable. Use this theorem in contexts where df-cleq or ax-ext is not referenced elsewhere in your proof. It is proven from a specific implementation (class builder, axiom df-clab ) of the primitive term x e. A . (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	iseqsetv-clel	|- ( E. x x = A <-> E. y y = A )

Proof

Step	Hyp	Ref	Expression
1		issettru	|- ( E. x x = A <-> A e. { z | T. } )
2		issettru	|- ( E. y y = A <-> A e. { z | T. } )
3	1 2	bitr4i	|- ( E. x x = A <-> E. y y = A )