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

Theorem nfand 2008
 Description: If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfand.1
nfand.2
Assertion
Ref Expression
nfand

Proof of Theorem nfand
StepHypRef Expression
1 df-an 373 . 2
2 nfand.1 . . . 4
3 nfand.2 . . . . 5
43nfnd 1984 . . . 4
52, 4nfimd 2000 . . 3
65nfnd 1984 . 2
71, 6nfxfrd 1697 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 371  wnf 1667 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933 This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668 This theorem is referenced by:  nf3and  2009  nfbid  2016  nfeld  2600  nfreud  2963  nfrmod  2964  nfrmo  2966  nfrab  2972  nfifd  3909  nfdisj  4385  dfid3  4750  nfriotad  6260  axrepndlem1  9017  axrepndlem2  9018  axunndlem1  9020  axunnd  9021  axregndlem2  9028  axinfndlem1  9030  axinfnd  9031  axacndlem4  9035  axacndlem5  9036  axacnd  9037  riotasv2d  32529
 Copyright terms: Public domain W3C validator