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

Theorem nfor 1935
Description: If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nf.1
nf.2
Assertion
Ref Expression
nfor

Proof of Theorem nfor
StepHypRef Expression
1 df-or 370 . 2
2 nf.1 . . . 4
32nfn 1901 . . 3
4 nf.2 . . 3
53, 4nfim 1920 . 2
61, 5nfxfr 1645 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368  F/wnf 1616
This theorem is referenced by:  nf3or  1936  axi12  2433  nfun  3659  nfpr  4076  rabsnifsb  4098  disjxun  4450  fsuppmapnn0fiubex  12098  nfsum1  13512  nfsum  13513  nfcprod1  13717  nfcprod  13718  fdc1  30239  dvdsrabdioph  30743
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-12 1854
This theorem depends on definitions:  df-bi 185  df-or 370  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator