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 -> C = D )
Assertion	rspceeqv	|- ( ( A e. B /\ E = D ) -> E. x e. B E = C )

Proof

Step	Hyp	Ref	Expression
1		rspceeqv.1	|- ( x = A -> C = D )
2	1	eqeq2d	|- ( x = A -> ( E = C <-> E = D ) )
3	2	rspcev	|- ( ( A e. B /\ E = D ) -> E. x e. B E = C )