Metamath Proof Explorer


Theorem wl-nfalv

Description: If x is not present in ph , it is not free in A. y ph . (Contributed by Wolf Lammen, 11-Jan-2020)

Ref Expression
Assertion wl-nfalv x y φ

Proof

Step Hyp Ref Expression
1 ax-5 φ x φ
2 1 hbal y φ x y φ
3 2 nf5i x y φ