Metamath Proof Explorer


Theorem exlimiieq1

Description: Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018)

Ref Expression
Hypotheses exlimiieq1.1 x φ
exlimiieq1.2 x = y φ
Assertion exlimiieq1 φ

Proof

Step Hyp Ref Expression
1 exlimiieq1.1 x φ
2 exlimiieq1.2 x = y φ
3 ax6e x x = y
4 1 2 3 exlimii φ