Metamath Proof Explorer


Theorem rspcedeq1vd

Description: Restricted existential specialization, using implicit substitution. Variant of rspcedvd for equations, in which the left hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019)

Ref Expression
Hypotheses rspcedeqvd.1 φ A B
rspcedeqvd.2 φ x = A C = D
Assertion rspcedeq1vd φ x B C = D

Proof

Step Hyp Ref Expression
1 rspcedeqvd.1 φ A B
2 rspcedeqvd.2 φ x = A C = D
3 2 eqeq1d φ x = A C = D D = D
4 eqidd φ D = D
5 1 3 4 rspcedvd φ x B C = D