Theorem nfal 2153

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

Hypothesis

Ref	Expression
nfal.1	|- F/ x ph

Assertion

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

Proof of Theorem nfal

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

Syntax hints:   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfex  2154  nfnf  2158  nfaldOLD  2166  nfa2OLD  2168  aaan  2170  cbv3v  2172  pm11.53  2179  19.12vv  2180  cbv3  2265  cbval2  2279  nfsb4t  2389  euf  2478  mo2  2479  2eu3  2555  bm1.1  2607  nfnfc1  2767  nfnfc  2774  nfnfcALT  2775  sbcnestgf  3995  dfnfc2OLD  4455  nfdisj  4632  nfdisj1  4633  axrep1  4772  axrep2  4773  axrep3  4774  axrep4  4775  nffr  5088  zfcndrep  9436  zfcndinf  9440  mreexexd  16308  mreexexdOLD  16309  mptelee  25775  mo5f  29324  19.12b  31707  bj-cbv2v  32732  bj-cbval2v  32737  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  bj-axrep4  32791  ax11-pm2  32823  bj-nfnfc  32853  wl-sb8t  33333  wl-mo2tf  33353  wl-eutf  33355  wl-mo2t  33357  wl-mo3t  33358  wl-sb8eut  33359  mpt2bi123f  33971  pm11.57  38589  pm11.59  38591  nfsetrecs  42433