Metamath Proof Explorer


Theorem reuxfr1ds

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Use reuhypd to eliminate the second hypothesis. (Contributed by NM, 16-Jan-2012)

Ref Expression
Hypotheses reuxfr1ds.1 φyCAB
reuxfr1ds.2 φxB∃!yCx=A
reuxfr1ds.3 x=Aψχ
Assertion reuxfr1ds φ∃!xBψ∃!yCχ

Proof

Step Hyp Ref Expression
1 reuxfr1ds.1 φyCAB
2 reuxfr1ds.2 φxB∃!yCx=A
3 reuxfr1ds.3 x=Aψχ
4 3 adantl φx=Aψχ
5 1 2 4 reuxfr1d φ∃!xBψ∃!yCχ