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	$$⊢\exists xx=A\leftrightarrow \exists yy=A$$

Proof

Step	Hyp	Ref	Expression
1		iseqsetvlem	$$⊢\exists xx=A\leftrightarrow \exists zz=A$$
2		iseqsetvlem	$$⊢\exists yy=A\leftrightarrow \exists zz=A$$
3	1 2	bitr4i	$$⊢\exists xx=A\leftrightarrow \exists yy=A$$