Theorem nfal 1947

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

Hypothesis

Ref	Expression
nfal.1

Assertion

Ref	Expression
nfal

Proof of Theorem nfal

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4
2	1	nfri 1874	. . 3
3	2	hbal 1844	. 2
4	3	nfi 1623	1

Syntax hints:  A.wal 1393  F/wnf 1616

This theorem is referenced by:  nfnf  1949  nfald  1951  nfa2  1953  aaan  1975  pm11.53  1983  19.12vv  1986  cbv3  2015  cbval2  2027  nfsb4t  2130  euf  2292  mo2  2293  2eu3  2379  bm1.1  2440  bm1.1OLD  2441  nfnfc1  2622  nfnfc  2628  nfnfcALT  2629  nfeqOLD  2631  sbcnestgf  3839  dfnfc2  4267  nfdisj  4434  nfdisj1  4435  axrep1  4564  axrep2  4565  axrep3  4566  axrep4  4567  nffr  4858  zfcndrep  9013  zfcndinf  9017  mreexexd  15045  mptelee  24198  mo5f  27383  19.12b  29234  wl-sb8t  30000  wl-mo2t  30020  wl-mo3t  30021  wl-sb8eut  30022  mpt2bi123f  30571  pm11.57  31295  pm11.59  31297  bj-cbv3v  34288  bj-cbv2v  34295  bj-cbval2v  34302  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  bj-axrep4  34377  ax11-pm2  34409  bj-nfnfc  34429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-11 1842  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617