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

Theorem nfne 3043
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 2941 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2919 . . 3 𝑥 𝐴 = 𝐵
54nfn 1857 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1853 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1540  wnf 1783  wnfc 2890  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-nfc 2892  df-ne 2941
This theorem is referenced by:  cantnflem1  9729  ac6c4  10521  fproddiv  15997  fprodn0  16015  fproddivf  16023  mreiincl  17639  lss1d  20961  iunconn  23436  restmetu  24583  coeeq2  26281  sltval2  27701  fedgmullem2  33681  bnj1534  34867  bnj1542  34871  bnj1398  35048  bnj1445  35058  bnj1449  35062  bnj1312  35072  bnj1525  35083  cvmcov  35268  nfwlim  35823  finminlem  36319  finxpreclem2  37391  poimirlem25  37652  poimirlem26  37653  poimirlem28  37655  cdleme40m  40469  cdleme40n  40470  dihglblem5  41300  iunconnlem2  44955  eliuniin2  45125  disjf1  45188  disjrnmpt2  45193  disjinfi  45197  allbutfiinf  45431  fsumiunss  45590  idlimc  45641  0ellimcdiv  45664  stoweidlem31  46046  stoweidlem58  46073  fourierdlem31  46153  sge0iunmpt  46433
  Copyright terms: Public domain W3C validator