# Metamath Proof Explorer

## Theorem rspcimedv

Description: Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses rspcimdv.1 ${⊢}{\phi }\to {A}\in {B}$
rspcimedv.2 ${⊢}\left({\phi }\wedge {x}={A}\right)\to \left({\chi }\to {\psi }\right)$
Assertion rspcimedv ${⊢}{\phi }\to \left({\chi }\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 rspcimdv.1 ${⊢}{\phi }\to {A}\in {B}$
2 rspcimedv.2 ${⊢}\left({\phi }\wedge {x}={A}\right)\to \left({\chi }\to {\psi }\right)$
3 2 con3d ${⊢}\left({\phi }\wedge {x}={A}\right)\to \left(¬{\psi }\to ¬{\chi }\right)$
4 1 3 rspcimdv ${⊢}{\phi }\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }\to ¬{\chi }\right)$
5 4 con2d ${⊢}{\phi }\to \left({\chi }\to ¬\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }\right)$
6 dfrex2 ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }$
7 5 6 syl6ibr ${⊢}{\phi }\to \left({\chi }\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$