Metamath Proof Explorer

Theorem exsbim

Description: One direction of the equivalence in exsb is based on fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023)

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

Proof

Step Hyp Ref Expression
1 alequexv 
 |-  ( A. x ( x = y -> ph ) -> E. x ph )
2 1 exlimiv 
 |-  ( E. y A. x ( x = y -> ph ) -> E. x ph )