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

Theorem nfand 1843
 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 361 . 2
2 nfand.1 . . . 4
3 nfand.2 . . . . 5
43nfnd 1809 . . . 4
52, 4nfimd 1827 . . 3
65nfnd 1809 . 2
71, 6nfxfrd 1580 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359  wnf 1553 This theorem is referenced by:  nf3and  1844  nfbid  1854  nfeld  2586  nfreud  2872  nfrmod  2873  nfrmo  2875  nfrab  2881  nfifd  3754  nfdisj  4186  dfid3  4491  nfriotad  6550  riotasv2d  6586  riotasv3dOLD  6591  axrepndlem1  8459  axrepndlem2  8460  axunndlem1  8462  axunnd  8463  axregndlem2  8470  axinfndlem1  8472  axinfnd  8473  axacndlem4  8477  axacndlem5  8478  axacnd  8479 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
 Copyright terms: Public domain W3C validator