Metamath Proof Explorer


Theorem ax5ea

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, 28-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 ax5e
 |-  ( E. x ph -> ph )
2 ax-5
 |-  ( ph -> A. x ph )
3 1 2 syl
 |-  ( E. x ph -> A. x ph )