Metamath Proof Explorer

Theorem nfal

Description: If x is not free in ph , it is not free in A. y ph . (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypothesis nfal.1 
|- F/ x ph
Assertion nfal 
|- F/ x A. y ph

Proof

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