Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfexd Unicode version

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
StepHypRef Expression
1 df-ex 1613 . 2
2 nfald.1 . . . 4
3 nfald.2 . . . . 5
43nfnd 1902 . . . 4
52, 4nfald 1951 . . 3
65nfnd 1902 . 2
71, 6nfxfrd 1646 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator