Metamath Proof Explorer


Theorem reueq1f

Description: Equality theorem for restricted unique existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 5-Apr-2004) (Revised by Andrew Salmon, 11-Jul-2011)

Ref Expression
Hypotheses rmoeq1f.1 _xA
rmoeq1f.2 _xB
Assertion reueq1f A=B∃!xAφ∃!xBφ

Proof

Step Hyp Ref Expression
1 rmoeq1f.1 _xA
2 rmoeq1f.2 _xB
3 1 2 rexeqf A=BxAφxBφ
4 1 2 rmoeq1f A=B*xAφ*xBφ
5 3 4 anbi12d A=BxAφ*xAφxBφ*xBφ
6 reu5 ∃!xAφxAφ*xAφ
7 reu5 ∃!xBφxBφ*xBφ
8 5 6 7 3bitr4g A=B∃!xAφ∃!xBφ