Theorem iseqsetvlem

Description: Lemma for iseqsetv-cleq . (Contributed by Wolf Lammen, 17-Aug-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	iseqsetvlem	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑧 𝑧 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝐴 ↔ 𝑧 = 𝐴 ) )
2	1	cbvexvw	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑧 𝑧 = 𝐴 )