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

Theorem nfne 3119
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 3017 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2991 . . 3 𝑥 𝐴 = 𝐵
54nfn 1848 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1844 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1528  wnf 1775  wnfc 2961  wne 3016
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 2793
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 2814  df-nfc 2963  df-ne 3017
This theorem is referenced by:  cantnflem1  9141  ac6c4  9892  fproddiv  15305  fprodn0  15323  fproddivf  15331  mreiincl  16857  lss1d  19666  iunconn  21966  restmetu  23109  coeeq2  24761  fedgmullem2  30926  bnj1534  32025  bnj1542  32029  bnj1398  32204  bnj1445  32214  bnj1449  32218  bnj1312  32228  bnj1525  32239  cvmcov  32408  nfwlim  33007  sltval2  33061  finminlem  33564  finxpreclem2  34554  poimirlem25  34799  poimirlem26  34800  poimirlem28  34802  cdleme40m  37485  cdleme40n  37486  dihglblem5  38316  iunconnlem2  41149  eliuniin2  41267  suprnmpt  41310  disjf1  41323  disjrnmpt2  41329  disjinfi  41334  allbutfiinf  41574  fsumiunss  41736  idlimc  41787  0ellimcdiv  41810  stoweidlem31  42197  stoweidlem58  42224  fourierdlem31  42304  sge0iunmpt  42581
  Copyright terms: Public domain W3C validator