Metamath Proof Explorer


Theorem reu8

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

Ref Expression
Hypothesis rmo4.1 x = y φ ψ
Assertion reu8 ∃! x A φ x A φ y A ψ x = y

Proof

Step Hyp Ref Expression
1 rmo4.1 x = y φ ψ
2 1 cbvreuvw ∃! x A φ ∃! y A ψ
3 reu6 ∃! y A ψ x A y A ψ y = x
4 dfbi2 ψ y = x ψ y = x y = x ψ
5 4 ralbii y A ψ y = x y A ψ y = x y = x ψ
6 r19.26 y A ψ y = x y = x ψ y A ψ y = x y A y = x ψ
7 ancom φ y A ψ x = y y A ψ x = y φ
8 equcom x = y y = x
9 8 imbi2i ψ x = y ψ y = x
10 9 ralbii y A ψ x = y y A ψ y = x
11 10 a1i x A y A ψ x = y y A ψ y = x
12 biimt x A φ x A φ
13 df-ral y A y = x ψ y y A y = x ψ
14 bi2.04 y A y = x ψ y = x y A ψ
15 14 albii y y A y = x ψ y y = x y A ψ
16 eleq1w x = y x A y A
17 16 1 imbi12d x = y x A φ y A ψ
18 17 bicomd x = y y A ψ x A φ
19 18 equcoms y = x y A ψ x A φ
20 19 equsalvw y y = x y A ψ x A φ
21 13 15 20 3bitrri x A φ y A y = x ψ
22 12 21 bitrdi x A φ y A y = x ψ
23 11 22 anbi12d x A y A ψ x = y φ y A ψ y = x y A y = x ψ
24 7 23 syl5bb x A φ y A ψ x = y y A ψ y = x y A y = x ψ
25 6 24 bitr4id x A y A ψ y = x y = x ψ φ y A ψ x = y
26 5 25 syl5bb x A y A ψ y = x φ y A ψ x = y
27 26 rexbiia x A y A ψ y = x x A φ y A ψ x = y
28 2 3 27 3bitri ∃! x A φ x A φ y A ψ x = y