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 
|- F/ x A. y ph

Proof

Step Hyp Ref Expression
1 ax-5 
 |-  ( ph -> A. x ph )
2 1 hbal 
 |-  ( A. y ph -> A. x A. y ph )
3 2 nf5i 
 |-  F/ x A. y ph