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

Theorem nfne 3116
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 3014 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2988 . . 3 𝑥 𝐴 = 𝐵
54nfn 1848 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1844 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1528  wnf 1775  wnfc 2958  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-cleq 2811  df-nfc 2960  df-ne 3014
This theorem is referenced by:  cantnflem1  9140  ac6c4  9891  fproddiv  15303  fprodn0  15321  fproddivf  15329  mreiincl  16855  lss1d  19664  iunconn  21964  restmetu  23107  coeeq2  24759  fedgmullem2  30925  bnj1534  32024  bnj1542  32028  bnj1398  32203  bnj1445  32213  bnj1449  32217  bnj1312  32227  bnj1525  32238  cvmcov  32407  nfwlim  33006  sltval2  33060  finminlem  33563  finxpreclem2  34553  poimirlem25  34798  poimirlem26  34799  poimirlem28  34801  cdleme40m  37483  cdleme40n  37484  dihglblem5  38314  iunconnlem2  41146  eliuniin2  41263  suprnmpt  41306  disjf1  41319  disjrnmpt2  41325  disjinfi  41330  allbutfiinf  41570  fsumiunss  41732  idlimc  41783  0ellimcdiv  41806  stoweidlem31  42193  stoweidlem58  42220  fourierdlem31  42300  sge0iunmpt  42577
  Copyright terms: Public domain W3C validator