# Metamath Proof Explorer

## Theorem sbhypf

Description: Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004)

Ref Expression
Hypotheses sbhypf.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
sbhypf.2 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
Assertion sbhypf ${⊢}{y}={A}\to \left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 sbhypf.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
2 sbhypf.2 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
3 eqeq1 ${⊢}{x}={y}\to \left({x}={A}↔{y}={A}\right)$
4 3 equsexvw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {x}={A}\right)↔{y}={A}$
5 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
6 5 1 nfbi ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$
7 sbequ12 ${⊢}{x}={y}\to \left({\phi }↔\left[{y}/{x}\right]{\phi }\right)$
8 7 bicomd ${⊢}{x}={y}\to \left(\left[{y}/{x}\right]{\phi }↔{\phi }\right)$
9 8 2 sylan9bb ${⊢}\left({x}={y}\wedge {x}={A}\right)\to \left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$
10 6 9 exlimi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {x}={A}\right)\to \left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$
11 4 10 sylbir ${⊢}{y}={A}\to \left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$