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

Theorem nfne 3042
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 2941 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2917 . . 3 𝑥 𝐴 = 𝐵
54nfn 1861 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1856 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1542  wnf 1786  wnfc 2884  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-nfc 2886  df-ne 2941
This theorem is referenced by:  cantnflem1  9630  ac6c4  10422  fproddiv  15849  fprodn0  15867  fproddivf  15875  mreiincl  17481  lss1d  20439  iunconn  22795  restmetu  23942  coeeq2  25619  sltval2  27020  fedgmullem2  32382  bnj1534  33522  bnj1542  33526  bnj1398  33703  bnj1445  33713  bnj1449  33717  bnj1312  33727  bnj1525  33738  cvmcov  33914  nfwlim  34453  finminlem  34836  finxpreclem2  35907  poimirlem25  36149  poimirlem26  36150  poimirlem28  36152  cdleme40m  38976  cdleme40n  38977  dihglblem5  39807  iunconnlem2  43305  eliuniin2  43418  disjf1  43489  disjrnmpt2  43495  disjinfi  43500  allbutfiinf  43741  fsumiunss  43902  idlimc  43953  0ellimcdiv  43976  stoweidlem31  44358  stoweidlem58  44385  fourierdlem31  44465  sge0iunmpt  44745
  Copyright terms: Public domain W3C validator