# Metamath Proof Explorer

## Theorem sbbibOLD

Description: Obsolete version of sbbib as of 4-Sep-2023. (Contributed by AV, 6-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses sbbibOLD.y ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
sbbibOLD.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion sbbibOLD ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 sbbibOLD.y ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 sbbibOLD.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
4 3 2 nfbi ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$
5 4 nf5ri ${⊢}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$
6 5 hbal ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$
7 sbcov ${⊢}\left[{x}/{y}\right]\left[{y}/{x}\right]{\phi }↔\left[{x}/{y}\right]{\phi }$
8 1 sbf ${⊢}\left[{x}/{y}\right]{\phi }↔{\phi }$
9 7 8 bitri ${⊢}\left[{x}/{y}\right]\left[{y}/{x}\right]{\phi }↔{\phi }$
10 spsbbi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)\to \left(\left[{x}/{y}\right]\left[{y}/{x}\right]{\phi }↔\left[{x}/{y}\right]{\psi }\right)$
11 9 10 bitr3id ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)\to \left({\phi }↔\left[{x}/{y}\right]{\psi }\right)$
12 6 11 alrimih ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)$
13 nfs1v ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{x}/{y}\right]{\psi }$
14 1 13 nfbi ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)$
15 14 nf5ri ${⊢}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)$
16 15 hbal ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)$
17 spsbbi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)\to \left(\left[{y}/{x}\right]{\phi }↔\left[{y}/{x}\right]\left[{x}/{y}\right]{\psi }\right)$
18 sbcov ${⊢}\left[{y}/{x}\right]\left[{x}/{y}\right]{\psi }↔\left[{y}/{x}\right]{\psi }$
19 2 sbf ${⊢}\left[{y}/{x}\right]{\psi }↔{\psi }$
20 18 19 bitri ${⊢}\left[{y}/{x}\right]\left[{x}/{y}\right]{\psi }↔{\psi }$
21 17 20 syl6bb ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)\to \left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$
22 16 21 alrimih ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)$
23 12 22 impbii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{\psi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔\left[{x}/{y}\right]{\psi }\right)$