Metamath Proof Explorer


Theorem nfv

Description: If x is not present in ph , then x is not free in ph . (Contributed by Mario Carneiro, 11-Aug-2016) Definition change. (Revised by Wolf Lammen, 12-Sep-2021)

Ref Expression
Assertion nfv
|- F/ x ph

Proof

Step Hyp Ref Expression
1 ax5ea
 |-  ( E. x ph -> A. x ph )
2 1 nfi
 |-  F/ x ph