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	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		iseqsetvlem	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑧 𝑧 = 𝐴 )
2		iseqsetvlem	⊢ ( ∃ 𝑦 𝑦 = 𝐴 ↔ ∃ 𝑧 𝑧 = 𝐴 )
3	1 2	bitr4i	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑦 = 𝐴 )