Metamath Proof Explorer


Theorem rmoeq1f

Description: Equality theorem for restricted at-most-one quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Alexander van der Vekens, 17-Jun-2017)

Ref Expression
Hypotheses raleq1f.1 _xA
raleq1f.2 _xB
Assertion rmoeq1f A=B*xAφ*xBφ

Proof

Step Hyp Ref Expression
1 raleq1f.1 _xA
2 raleq1f.2 _xB
3 1 2 nfeq xA=B
4 eleq2 A=BxAxB
5 4 anbi1d A=BxAφxBφ
6 3 5 mobid A=B*xxAφ*xxBφ
7 df-rmo *xAφ*xxAφ
8 df-rmo *xBφ*xxBφ
9 6 7 8 3bitr4g A=B*xAφ*xBφ