Theorem iseqsetv-cleq

Description: Alternate proof of iseqsetv-clel . The expression E. x x = A does not depend on a particular choice of the set variable. The proof here avoids df-clab , df-clel and ax-8 , but instead is based on ax-9 , ax-ext and df-cleq . In particular it still accepts x e. A being a primitive syntax term, not assuming any specific semantics (like elementhood in some form).

Use it in contexts where you want to avoid df-clab , or you need df-cleq anyway. See the alternative version , not using df-cleq or ax-ext or ax-9 . (Contributed by Wolf Lammen, 6-Aug-2025) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		iseqsetvlem	|- ( E. x x = A <-> E. z z = A )
2		iseqsetvlem	|- ( E. y y = A <-> E. z z = A )
3	1 2	bitr4i	|- ( E. x x = A <-> E. y y = A )