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

Theorem nfne 3048
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 2948 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2927 . . 3 𝑥 𝐴 = 𝐵
54nfn 1867 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1863 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1550  wnf 1793  wnfc 2899  wne 2947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1553  df-ex 1790  df-nf 1794  df-cleq 2744  df-nfc 2901  df-ne 2948
This theorem is referenced by:  cantnflem1  9630  ac6c4  10424  fproddiv  15963  fprodn0  15981  fproddivf  15989  mreiincl  17596  lss1d  20999  iunconn  23457  restmetu  24599  coeeq2  26271  ltsval2  27686  fedgmullem2  33871  bnj1534  35095  bnj1542  35099  bnj1398  35276  bnj1445  35286  bnj1449  35290  bnj1312  35300  bnj1525  35311  cvmcov  35551  nfwlim  36108  finminlem  36616  finxpreclem2  37822  poimirlem25  38082  poimirlem26  38083  poimirlem28  38085  cdleme40m  41029  cdleme40n  41030  dihglblem5  41860  iunconnlem2  45448  eliuniin2  45636  disjf1  45699  disjrnmpt2  45704  disjinfi  45708  allbutfiinf  45932  fsumiunss  46089  idlimc  46140  0ellimcdiv  46161  stoweidlem31  46543  stoweidlem58  46570  fourierdlem31  46650  sge0iunmpt  46930
  Copyright terms: Public domain W3C validator