Theorem nfexd 1952

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

Hypotheses

Ref	Expression
nfald.1
nfald.2

Assertion

Ref	Expression
nfexd

Proof of Theorem nfexd

Step	Hyp	Ref	Expression
1		df-ex 1613	. 2
2		nfald.1	. . . 4
3		nfald.2	. . . . 5
4	3	nfnd 1902	. . . 4
5	2, 4	nfald 1951	. . 3
6	5	nfnd 1902	. 2
7	1, 6	nfxfrd 1646	1

Syntax hints:  -.wn 3  ->wi 4  A.wal 1393  E.wex 1612  F/wnf 1616

This theorem is referenced by:  nfeud2  2296  nfeld  2627  axrepndlem1  8988  axrepndlem2  8989  axunndlem1  8991  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  19.9d2rf  27377  hbexg  33329

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