Theorem nfald 1951

Description: If is not free in , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)

Hypotheses

Ref	Expression
nfald.1
nfald.2

Assertion

Ref	Expression
nfald

Proof of Theorem nfald

Step	Hyp	Ref	Expression
1		nfald.1	. . 3
2		nfald.2	. . 3
3	1, 2	alrimi 1877	. 2
4		nfnf1 1899	. . . 4
5	4	nfal 1947	. . 3
6		hba1 1896	. . . 4
7		sp 1859	. . . . 5
8	7	nfrd 1875	. . . 4
9	6, 8	hbald 1848	. . 3
10	5, 9	nfd 1878	. 2
11	3, 10	syl 16	1

Syntax hints:  ->wi 4  A.wal 1393  F/wnf 1616

This theorem is referenced by:  nfexd  1952  dvelimhw  1955  nfald2  2073  nfeqd  2626  axrepndlem1  8988  axrepndlem2  8989  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem4  8998  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  wl-mo2dnae  30019  wl-mo2t  30020

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-10 1837  ax-11 1842  ax-12 1854

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