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

Theorem nfne 2882
 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 2782 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2762 . . 3 𝑥 𝐴 = 𝐵
54nfn 1768 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1771 1 𝑥 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1475  Ⅎwnf 1699  Ⅎwnfc 2738   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-nfc 2740  df-ne 2782 This theorem is referenced by:  cantnflem1  8469  ac6c4  9186  fproddiv  14530  fprodn0  14548  fproddivf  14557  mreiincl  16079  lss1d  18784  iuncon  21041  restmetu  22185  coeeq2  23802  bnj1534  30177  bnj1542  30181  bnj1398  30356  bnj1445  30366  bnj1449  30370  bnj1312  30380  bnj1525  30391  cvmcov  30499  nfwlim  31012  sltval2  31053  nobndlem5  31095  finminlem  31482  finxpreclem2  32403  poimirlem25  32604  poimirlem26  32605  poimirlem28  32607  cdleme40m  34773  cdleme40n  34774  dihglblem5  35605  iunconlem2  38193  eliuniin2  38335  suprnmpt  38350  disjf1  38364  disjrnmpt2  38370  disjinfi  38375  fsumiunss  38642  idlimc  38693  0ellimcdiv  38716  stoweidlem31  38924  stoweidlem58  38951  fourierdlem31  39031  sge0iunmpt  39311
 Copyright terms: Public domain W3C validator