This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iseqsetvlem

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

		Ref	Expression
	Assertion	iseqsetvlem	$⊢ \exists x x = A \leftrightarrow \exists z z = A$

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ x = z \to (x = A \leftrightarrow z = A)$
2	1	cbvexvw	$⊢ \exists x x = A \leftrightarrow \exists z z = A$