Metamath Proof Explorer


Theorem reu7

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

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

Proof

Step Hyp Ref Expression
1 rmo4.1 x = y φ ψ
2 reu3 ∃! x A φ x A φ z A x A φ x = z
3 equequ1 x = y x = z y = z
4 equcom y = z z = y
5 3 4 bitrdi x = y x = z z = y
6 1 5 imbi12d x = y φ x = z ψ z = y
7 6 cbvralvw x A φ x = z y A ψ z = y
8 7 rexbii z A x A φ x = z z A y A ψ z = y
9 equequ1 z = x z = y x = y
10 9 imbi2d z = x ψ z = y ψ x = y
11 10 ralbidv z = x y A ψ z = y y A ψ x = y
12 11 cbvrexvw z A y A ψ z = y x A y A ψ x = y
13 8 12 bitri z A x A φ x = z x A y A ψ x = y
14 13 anbi2i x A φ z A x A φ x = z x A φ x A y A ψ x = y
15 2 14 bitri ∃! x A φ x A φ x A y A ψ x = y