# Metamath Proof Explorer

## Theorem rmo3f

Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmo3f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
rmo3f.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
rmo3f.3 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 rmo3f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 rmo3f.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
3 rmo3f.3 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 df-rmo ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
5 sban ${⊢}\left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)↔\left(\left[{y}/{x}\right]{x}\in {A}\wedge \left[{y}/{x}\right]{\phi }\right)$
6 1 clelsb3fw ${⊢}\left[{y}/{x}\right]{x}\in {A}↔{y}\in {A}$
7 6 anbi1i ${⊢}\left(\left[{y}/{x}\right]{x}\in {A}\wedge \left[{y}/{x}\right]{\phi }\right)↔\left({y}\in {A}\wedge \left[{y}/{x}\right]{\phi }\right)$
8 5 7 bitri ${⊢}\left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)↔\left({y}\in {A}\wedge \left[{y}/{x}\right]{\phi }\right)$
9 8 anbi2i ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)\right)↔\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {A}\wedge \left[{y}/{x}\right]{\phi }\right)\right)$
10 an4 ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {A}\wedge \left[{y}/{x}\right]{\phi }\right)\right)↔\left(\left({x}\in {A}\wedge {y}\in {A}\right)\wedge \left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\right)$
11 ancom ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)↔\left({y}\in {A}\wedge {x}\in {A}\right)$
12 11 anbi1i ${⊢}\left(\left({x}\in {A}\wedge {y}\in {A}\right)\wedge \left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\right)↔\left(\left({y}\in {A}\wedge {x}\in {A}\right)\wedge \left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\right)$
13 9 10 12 3bitri ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)\right)↔\left(\left({y}\in {A}\wedge {x}\in {A}\right)\wedge \left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\right)$
14 13 imbi1i ${⊢}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)\right)\to {x}={y}\right)↔\left(\left(\left({y}\in {A}\wedge {x}\in {A}\right)\wedge \left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\right)\to {x}={y}\right)$
15 impexp ${⊢}\left(\left(\left({y}\in {A}\wedge {x}\in {A}\right)\wedge \left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\right)\to {x}={y}\right)↔\left(\left({y}\in {A}\wedge {x}\in {A}\right)\to \left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)$
16 impexp ${⊢}\left(\left({y}\in {A}\wedge {x}\in {A}\right)\to \left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)↔\left({y}\in {A}\to \left({x}\in {A}\to \left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)\right)$
17 14 15 16 3bitri ${⊢}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)\right)\to {x}={y}\right)↔\left({y}\in {A}\to \left({x}\in {A}\to \left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)\right)$
18 17 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)\right)\to {x}={y}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to \left({x}\in {A}\to \left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)\right)$
19 df-ral ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to \left({x}\in {A}\to \left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)\right)$
20 2 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
21 20 r19.21 ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)↔\left({x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)$
22 18 19 21 3bitr2i ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)\right)\to {x}={y}\right)↔\left({x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)$
23 22 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)\right)\to {x}={y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)$
24 20 3 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
25 24 mo3 ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)\right)\to {x}={y}\right)$
26 df-ral ${⊢}\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}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)$
27 23 25 26 3bitr4i ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\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)$
28 4 27 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 \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)$