# Metamath Proof Explorer

## Theorem rspcebdv

Description: Restricted existential specialization, using implicit substitution in both directions. (Contributed by AV, 8-Jan-2022)

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

### Proof

Step Hyp Ref Expression
1 rspcdv.1 ${⊢}{\phi }\to {A}\in {B}$
2 rspcdv.2 ${⊢}\left({\phi }\wedge {x}={A}\right)\to \left({\psi }↔{\chi }\right)$
3 rspcebdv.1 ${⊢}\left({\phi }\wedge {\psi }\right)\to {x}={A}$
4 3 2 syldan ${⊢}\left({\phi }\wedge {\psi }\right)\to \left({\psi }↔{\chi }\right)$
5 4 biimpd ${⊢}\left({\phi }\wedge {\psi }\right)\to \left({\psi }\to {\chi }\right)$
6 5 expcom ${⊢}{\psi }\to \left({\phi }\to \left({\psi }\to {\chi }\right)\right)$
7 6 pm2.43b ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
8 7 rexlimdvw ${⊢}{\phi }\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\to {\chi }\right)$
9 1 2 rspcedv ${⊢}{\phi }\to \left({\chi }\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
10 8 9 impbid ${⊢}{\phi }\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔{\chi }\right)$