# Metamath Proof Explorer

## Theorem sb6fALT

Description: Alternate version of sb6f . (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 4-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dfsb1.p5 ${⊢}{\theta }↔\left(\left({x}={y}\to {\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\right)$
sb6fALT.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion sb6fALT ${⊢}{\theta }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$

### Proof

Step Hyp Ref Expression
1 dfsb1.p5 ${⊢}{\theta }↔\left(\left({x}={y}\to {\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\right)$
2 sb6fALT.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 biid ${⊢}\left(\left({x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)↔\left(\left({x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
4 2 nf5ri ${⊢}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 1 3 4 sbimiALT ${⊢}{\theta }\to \left(\left({x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
6 3 sb4aALT ${⊢}\left(\left({x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$
7 5 6 syl ${⊢}{\theta }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$
8 1 sb2ALT ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to {\theta }$
9 7 8 impbii ${⊢}{\theta }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$