Metamath Proof Explorer


Theorem reu4

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994)

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

Proof

Step Hyp Ref Expression
1 rmo4.1 x = y φ ψ
2 reu5 ∃! x A φ x A φ * x A φ
3 1 rmo4 * x A φ x A y A φ ψ x = y
4 3 anbi2i x A φ * x A φ x A φ x A y A φ ψ x = y
5 2 4 bitri ∃! x A φ x A φ x A y A φ ψ x = y