Metamath Proof Explorer

Theorem alequexv

Description: Version of equs4v with its consequence simplified by exsimpr . (Contributed by BJ, 9-Nov-2021)

Ref Expression
Assertion alequexv 
|- ( A. x ( x = y -> ph ) -> E. x ph )

Proof

Step Hyp Ref Expression
1 ax6ev 
 |-  E. x x = y
2 exim 
 |-  ( A. x ( x = y -> ph ) -> ( E. x x = y -> E. x ph ) )
3 1 2 mpi 
 |-  ( A. x ( x = y -> ph ) -> E. x ph )