Description: Restricted existential specialization, using implicit substitution. Variant of rspcedvd for equations, in which the right hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | rspcedeqvd.1 | |- ( ph -> A e. B ) |
|
| rspcedeqvd.2 | |- ( ( ph /\ x = A ) -> C = D ) |
||
| Assertion | rspcedeq2vd | |- ( ph -> E. x e. B C = D ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rspcedeqvd.1 | |- ( ph -> A e. B ) |
|
| 2 | rspcedeqvd.2 | |- ( ( ph /\ x = A ) -> C = D ) |
|
| 3 | 2 1 | rspcime | |- ( ph -> E. x e. B C = D ) |