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

Theorem nfne 2788
Description: Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfne.1
nfne.2
Assertion
Ref Expression
nfne

Proof of Theorem nfne
StepHypRef Expression
1 df-ne 2654 . 2
2 nfne.1 . . . 4
3 nfne.2 . . . 4
42, 3nfeq 2630 . . 3
54nfn 1901 . 2
61, 5nfxfr 1645 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  =wceq 1395  F/wnf 1616  F/_wnfc 2605  =/=wne 2652
This theorem is referenced by:  cantnflem1  8129  ac6c4  8882  fproddiv  13766  fprodn0  13783  mreiincl  14993  lss1d  17609  iuncon  19929  restmetu  21090  coeeq2  22639  cvmcov  28708  nfwlim  29378  sltval2  29416  nobndlem5  29456  finminlem  30136  suprnmpt  31451  fproddivf  31588  idlimc  31632  0ellimcdiv  31655  stoweidlem31  31813  stoweidlem58  31840  fourierdlem31  31920  iunconlem2  33735  bnj1534  33911  bnj1542  33915  bnj1398  34090  bnj1445  34100  bnj1449  34104  bnj1312  34114  bnj1525  34125  cdleme40m  36193  cdleme40n  36194  dihglblem5  37025
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  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-nfc 2607  df-ne 2654
  Copyright terms: Public domain W3C validator