Metamath Proof Explorer


Theorem exlimiieq2

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

Ref Expression
Hypotheses exlimiieq2.1
|- F/ y ph
exlimiieq2.2
|- ( x = y -> ph )
Assertion exlimiieq2
|- ph

Proof

Step Hyp Ref Expression
1 exlimiieq2.1
 |-  F/ y ph
2 exlimiieq2.2
 |-  ( x = y -> ph )
3 ax6er
 |-  E. y x = y
4 1 2 3 exlimii
 |-  ph