Metamath Proof Explorer

Theorem 2sb5nd

Description: Equivalence for double substitution 2sb5 without distinct x , y requirement. 2sb5nd is derived from 2sb5ndVD . (Contributed by Alan Sare, 30-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2sb5nd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)\to \left(\left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)\right)$

Proof

Step Hyp Ref Expression
1 ax6e2ndeq ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)$
2 anabs5 ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)$
3 2pm13.193 ${⊢}\left(\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)↔\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)$
4 3 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)$
5 nfs1v ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{v}/{y}\right]{\phi }$
6 5 nfsb ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }$
7 6 19.41 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)$
8 4 7 bitr3i ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)$
9 8 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)$
10 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }$
11 10 19.41 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)$
12 9 11 bitr2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)$
13 12 anbi2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)\right)$
14 2 13 bitr3i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)\right)$
15 pm5.32 ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to \left(\left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)\right)\right)↔\left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)\right)\right)$
16 14 15 mpbir ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to \left(\left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)\right)$
17 1 16 sylbi ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)\to \left(\left[{u}/{x}\right]\left[{v}/{y}\right]{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\wedge {\phi }\right)\right)$