Metamath Proof Explorer


Theorem rexeqi

Description: Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypothesis raleq1i.1 A=B
Assertion rexeqi xAφxBφ

Proof

Step Hyp Ref Expression
1 raleq1i.1 A=B
2 rexeq A=BxAφxBφ
3 1 2 ax-mp xAφxBφ