Metamath Proof Explorer

Theorem wl-mo2t

Description: Closed form of mof . (Contributed by Wolf Lammen, 18-Aug-2019)

Ref Expression
Assertion wl-mo2t ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)$

Proof

Step Hyp Ref Expression
1 df-mo ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {u}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={u}\right)$
2 nfnf1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 2 nfal ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
6 nfvd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}={u}$
7 5 6 nfimd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={u}\right)$
8 4 7 nfald ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={u}\right)$
9 equequ2 ${⊢}{u}={y}\to \left({x}={u}↔{x}={y}\right)$
10 9 imbi2d ${⊢}{u}={y}\to \left(\left({\phi }\to {x}={u}\right)↔\left({\phi }\to {x}={y}\right)\right)$
11 10 albidv ${⊢}{u}={y}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={u}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)$
12 11 a1i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({u}={y}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={u}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)\right)$
13 3 8 12 cbvexdw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {u}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={u}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)$
14 1 13 syl5bb ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)$