# Metamath Proof Explorer

## Theorem reu8

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006)

Ref Expression
Hypothesis rmo4.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion reu8 ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 rmo4.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 1 cbvreuvw ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$
3 reu6 ${⊢}\exists !{y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }↔{y}={x}\right)$
4 dfbi2 ${⊢}\left({\psi }↔{y}={x}\right)↔\left(\left({\psi }\to {y}={x}\right)\wedge \left({y}={x}\to {\psi }\right)\right)$
5 4 ralbii ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }↔{y}={x}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\psi }\to {y}={x}\right)\wedge \left({y}={x}\to {\psi }\right)\right)$
6 ancom ${⊢}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\wedge {\phi }\right)$
7 equcom ${⊢}{x}={y}↔{y}={x}$
8 7 imbi2i ${⊢}\left({\psi }\to {x}={y}\right)↔\left({\psi }\to {y}={x}\right)$
9 8 ralbii ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={x}\right)$
10 9 a1i ${⊢}{x}\in {A}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={x}\right)\right)$
11 biimt ${⊢}{x}\in {A}\to \left({\phi }↔\left({x}\in {A}\to {\phi }\right)\right)$
12 df-ral ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to {\psi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to \left({y}={x}\to {\psi }\right)\right)$
13 bi2.04 ${⊢}\left({y}\in {A}\to \left({y}={x}\to {\psi }\right)\right)↔\left({y}={x}\to \left({y}\in {A}\to {\psi }\right)\right)$
14 13 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to \left({y}={x}\to {\psi }\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to \left({y}\in {A}\to {\psi }\right)\right)$
15 eleq1w ${⊢}{x}={y}\to \left({x}\in {A}↔{y}\in {A}\right)$
16 15 1 imbi12d ${⊢}{x}={y}\to \left(\left({x}\in {A}\to {\phi }\right)↔\left({y}\in {A}\to {\psi }\right)\right)$
17 16 bicomd ${⊢}{x}={y}\to \left(\left({y}\in {A}\to {\psi }\right)↔\left({x}\in {A}\to {\phi }\right)\right)$
18 17 equcoms ${⊢}{y}={x}\to \left(\left({y}\in {A}\to {\psi }\right)↔\left({x}\in {A}\to {\phi }\right)\right)$
19 18 equsalvw ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to \left({y}\in {A}\to {\psi }\right)\right)↔\left({x}\in {A}\to {\phi }\right)$
20 12 14 19 3bitrri ${⊢}\left({x}\in {A}\to {\phi }\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to {\psi }\right)$
21 11 20 syl6bb ${⊢}{x}\in {A}\to \left({\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to {\psi }\right)\right)$
22 10 21 anbi12d ${⊢}{x}\in {A}\to \left(\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\wedge {\phi }\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={x}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to {\psi }\right)\right)\right)$
23 6 22 syl5bb ${⊢}{x}\in {A}\to \left(\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={x}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to {\psi }\right)\right)\right)$
24 r19.26 ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\psi }\to {y}={x}\right)\wedge \left({y}={x}\to {\psi }\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={x}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to {\psi }\right)\right)$
25 23 24 syl6rbbr ${⊢}{x}\in {A}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\psi }\to {y}={x}\right)\wedge \left({y}={x}\to {\psi }\right)\right)↔\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\right)\right)$
26 5 25 syl5bb ${⊢}{x}\in {A}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }↔{y}={x}\right)↔\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\right)\right)$
27 26 rexbiia ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }↔{y}={x}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\right)$
28 2 3 27 3bitri ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {x}={y}\right)\right)$