Metamath Proof Explorer


Theorem reueqd

Description: Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004)

Ref Expression
Hypothesis raleqd.1 A=Bφψ
Assertion reueqd A=B∃!xAφ∃!xBψ

Proof

Step Hyp Ref Expression
1 raleqd.1 A=Bφψ
2 reueq1 A=B∃!xAφ∃!xBφ
3 1 reubidv A=B∃!xBφ∃!xBψ
4 2 3 bitrd A=B∃!xAφ∃!xBψ