# Metamath Proof Explorer

## Theorem rmo4

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypothesis rmo4.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion rmo4 ${⊢}{\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 rmo4.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 df-rmo ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
3 an4 ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {A}\wedge {\psi }\right)\right)↔\left(\left({x}\in {A}\wedge {y}\in {A}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)$
4 ancom ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)↔\left({y}\in {A}\wedge {x}\in {A}\right)$
5 4 anbi1i ${⊢}\left(\left({x}\in {A}\wedge {y}\in {A}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)↔\left(\left({y}\in {A}\wedge {x}\in {A}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)$
6 3 5 bitri ${⊢}\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {A}\wedge {\psi }\right)\right)↔\left(\left({y}\in {A}\wedge {x}\in {A}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)$
7 6 imbi1i ${⊢}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {A}\wedge {\psi }\right)\right)\to {x}={y}\right)↔\left(\left(\left({y}\in {A}\wedge {x}\in {A}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\to {x}={y}\right)$
8 impexp ${⊢}\left(\left(\left({y}\in {A}\wedge {x}\in {A}\right)\wedge \left({\phi }\wedge {\psi }\right)\right)\to {x}={y}\right)↔\left(\left({y}\in {A}\wedge {x}\in {A}\right)\to \left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$
9 impexp ${⊢}\left(\left({y}\in {A}\wedge {x}\in {A}\right)\to \left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)↔\left({y}\in {A}\to \left({x}\in {A}\to \left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)\right)$
10 7 8 9 3bitri ${⊢}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {A}\wedge {\psi }\right)\right)\to {x}={y}\right)↔\left({y}\in {A}\to \left({x}\in {A}\to \left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)\right)$
11 10 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {A}\wedge {\psi }\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 {\psi }\right)\to {x}={y}\right)\right)\right)$
12 df-ral ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left(\left({\phi }\wedge {\psi }\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 {\psi }\right)\to {x}={y}\right)\right)\right)$
13 r19.21v ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)↔\left({x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$
14 11 12 13 3bitr2i ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left(\left({x}\in {A}\wedge {\phi }\right)\wedge \left({y}\in {A}\wedge {\psi }\right)\right)\to {x}={y}\right)↔\left({x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$
15 14 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}\in {A}\wedge {\psi }\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 {\psi }\right)\to {x}={y}\right)\right)$
16 eleq1w ${⊢}{x}={y}\to \left({x}\in {A}↔{y}\in {A}\right)$
17 16 1 anbi12d ${⊢}{x}={y}\to \left(\left({x}\in {A}\wedge {\phi }\right)↔\left({y}\in {A}\wedge {\psi }\right)\right)$
18 17 mo4 ${⊢}{\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}\in {A}\wedge {\psi }\right)\right)\to {x}={y}\right)$
19 df-ral ${⊢}\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)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$
20 15 18 19 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 {\psi }\right)\to {x}={y}\right)$
21 2 20 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)$