Metamath Proof Explorer

Theorem rmo4f

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by Thierry Arnoux, 11-Oct-2016) (Revised by Thierry Arnoux, 8-Mar-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmo4f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
rmo4f.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
rmo4f.3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
rmo4f.4 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion rmo4f ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)$

Proof

Step Hyp Ref Expression
1 rmo4f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 rmo4f.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
3 rmo4f.3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
4 rmo4f.4 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
5 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
6 1 2 5 rmo3f ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)$
7 3 4 sbiev ${⊢}\left[{y}/{x}\right]{\phi }↔{\psi }$
8 7 anbi2i ${⊢}\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)↔\left({\phi }\wedge {\psi }\right)$
9 8 imbi1i ${⊢}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)↔\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)$
10 9 2ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)$
11 6 10 bitri ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)$