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 x φ x φ


Step Hyp Ref Expression
1 ax5e x φ φ
2 ax-5 φ x φ
3 1 2 syl x φ x φ