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

Theorem nfne 2923
 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 2824 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2805 . . 3 𝑥 𝐴 = 𝐵
54nfn 1824 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1819 1 𝑥 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1523  Ⅎwnf 1748  Ⅎwnfc 2780   ≠ wne 2823 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-nfc 2782  df-ne 2824 This theorem is referenced by:  cantnflem1  8624  ac6c4  9341  fproddiv  14735  fprodn0  14753  fproddivf  14762  mreiincl  16303  lss1d  19011  iunconn  21279  restmetu  22422  coeeq2  24043  bnj1534  31049  bnj1542  31053  bnj1398  31228  bnj1445  31238  bnj1449  31242  bnj1312  31252  bnj1525  31263  cvmcov  31371  nfwlim  31892  sltval2  31934  finminlem  32437  finxpreclem2  33357  poimirlem25  33564  poimirlem26  33565  poimirlem28  33567  cdleme40m  36072  cdleme40n  36073  dihglblem5  36904  iunconnlem2  39485  eliuniin2  39617  suprnmpt  39669  disjf1  39683  disjrnmpt2  39689  disjinfi  39694  allbutfiinf  39960  fsumiunss  40125  idlimc  40176  0ellimcdiv  40199  stoweidlem31  40566  stoweidlem58  40593  fourierdlem31  40673  sge0iunmpt  40953
 Copyright terms: Public domain W3C validator