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

Theorem nfexd 2034
 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 1663 . 2
2 nfald.1 . . . 4
3 nfald.2 . . . . 5
43nfnd 1983 . . . 4
52, 4nfald 2033 . . 3
65nfnd 1983 . 2
71, 6nfxfrd 1696 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4  wal 1441  wex 1662  wnf 1666 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932 This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-nf 1667 This theorem is referenced by:  nfeud2  2310  nfeld  2599  axrepndlem1  9014  axrepndlem2  9015  axunndlem1  9017  axunnd  9018  axpowndlem2  9020  axpowndlem3  9021  axpowndlem4  9022  axregndlem2  9025  axinfndlem1  9027  axinfnd  9028  axacndlem4  9032  axacndlem5  9033  axacnd  9034  19.9d2rf  28105  hbexg  36917
 Copyright terms: Public domain W3C validator