Metamath Proof Explorer

Theorem ax5e

Description: A rephrasing of ax-5 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017)

Ref Expression
Assertion ax5e 
|- ( E. x ph -> ph )

Proof

Step Hyp Ref Expression
1 ax-5 
 |-  ( -. ph -> A. x -. ph )
2 eximal 
 |-  ( ( E. x ph -> ph ) <-> ( -. ph -> A. x -. ph ) )
3 1 2 mpbir 
 |-  ( E. x ph -> ph )