Metamath Proof Explorer

Theorem 19.8v

Description: Version of 19.8a with a disjoint variable condition, requiring fewer axioms. Converse of ax5e . (Contributed by BJ, 12-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 ax-5 
 |-  ( ph -> A. x ph )
2 1 19.8w 
 |-  ( ph -> E. x ph )