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

Metamath Proof Explorer

Theorem rexeqdv

Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007)

		Ref	Expression
	Hypothesis	raleqdv.1	$⊢ φ \to A = B$
	Assertion	rexeqdv	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists x \in B ψ)$

Step	Hyp	Ref	Expression
1		raleqdv.1	$⊢ φ \to A = B$
2		rexeq	$⊢ A = B \to (\exists x \in A ψ \leftrightarrow \exists x \in B ψ)$
3	1 2	syl	$⊢ φ \to (\exists x \in A ψ \leftrightarrow \exists x \in B ψ)$