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 x A φ x B φ

Proof

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