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

Theorem nfne 3087
 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 2988 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2968 . . 3 𝑥 𝐴 = 𝐵
54nfn 1858 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1854 1 𝑥 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1538  Ⅎwnf 1785  Ⅎwnfc 2936   ≠ wne 2987 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-nfc 2938  df-ne 2988 This theorem is referenced by:  cantnflem1  9139  ac6c4  9895  fproddiv  15310  fprodn0  15328  fproddivf  15336  mreiincl  16862  lss1d  19732  iunconn  22043  restmetu  23187  coeeq2  24849  fedgmullem2  31129  bnj1534  32250  bnj1542  32254  bnj1398  32431  bnj1445  32441  bnj1449  32445  bnj1312  32455  bnj1525  32466  cvmcov  32638  nfwlim  33237  sltval2  33291  finminlem  33794  finxpreclem2  34826  poimirlem25  35101  poimirlem26  35102  poimirlem28  35104  cdleme40m  37782  cdleme40n  37783  dihglblem5  38613  iunconnlem2  41684  eliuniin2  41798  suprnmpt  41841  disjf1  41852  disjrnmpt2  41858  disjinfi  41863  allbutfiinf  42100  fsumiunss  42260  idlimc  42311  0ellimcdiv  42334  stoweidlem31  42716  stoweidlem58  42743  fourierdlem31  42823  sge0iunmpt  43100
 Copyright terms: Public domain W3C validator