Description: If a formula holds for some value of a variable not occurring in it, then it holds for all values of that variable. (Contributed by BJ, 28Dec2020)
Ref  Expression  

Assertion  ax5ea   ( E. x ph > A. x ph ) 
Step  Hyp  Ref  Expression 

1  ax5e   ( E. x ph > ph ) 

2  ax5   ( ph > A. x ph ) 

3  1 2  syl   ( E. x ph > A. x ph ) 