# Metamath Proof Explorer

## Theorem rmo3

Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) Avoid ax-13 . (Revised by Wolf Lammen, 30-Apr-2023)

Ref Expression
Hypothesis rmo2.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion rmo3 ${⊢}{\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 rmo2.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 df-rmo ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
3 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)$
4 clelsb3 ${⊢}\left[{y}/{x}\right]{x}\in {A}↔{y}\in {A}$
5 4 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)$
6 3 5 bitri ${⊢}\left[{y}/{x}\right]\left({x}\in {A}\wedge {\phi }\right)↔\left({y}\in {A}\wedge \left[{y}/{x}\right]{\phi }\right)$
7 6 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)$
8 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)$
9 ancom ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)↔\left({y}\in {A}\wedge {x}\in {A}\right)$
10 9 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)$
11 7 8 10 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)$
12 11 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)$
13 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)$
14 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)$
15 12 13 14 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)$
16 15 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)$
17 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)$
18 r19.21v ${⊢}\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)$
19 16 17 18 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)$
20 19 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)$
21 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
22 21 1 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
23 22 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)$
24 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)$
25 20 23 24 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)$
26 2 25 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)$