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

Metamath Proof Explorer

Theorem rspceeqv

Description: Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022)

		Ref	Expression
	Hypothesis	rspceeqv.1	$⊢ x = A \to C = D$
	Assertion	rspceeqv	$⊢ (A \in B \land E = D) \to \exists x \in B E = C$

Step	Hyp	Ref	Expression
1		rspceeqv.1	$⊢ x = A \to C = D$
2	1	eqeq2d	$⊢ x = A \to (E = C \leftrightarrow E = D)$
3	2	rspcev	$⊢ (A \in B \land E = D) \to \exists x \in B E = C$