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

Theorem nfne 3042
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 2917 . . 3 𝑥 𝐴 = 𝐵
54nfn 1865 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1860 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1543  wnf 1791  wnfc 2884  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-cleq 2729  df-nfc 2886  df-ne 2941
This theorem is referenced by:  cantnflem1  9304  ac6c4  10095  fproddiv  15523  fprodn0  15541  fproddivf  15549  mreiincl  17099  lss1d  20000  iunconn  22325  restmetu  23468  coeeq2  25136  fedgmullem2  31425  bnj1534  32546  bnj1542  32550  bnj1398  32727  bnj1445  32737  bnj1449  32741  bnj1312  32751  bnj1525  32762  cvmcov  32938  nfwlim  33553  sltval2  33596  finminlem  34244  finxpreclem2  35298  poimirlem25  35539  poimirlem26  35540  poimirlem28  35542  cdleme40m  38218  cdleme40n  38219  dihglblem5  39049  iunconnlem2  42228  eliuniin2  42342  disjf1  42393  disjrnmpt2  42399  disjinfi  42404  allbutfiinf  42633  fsumiunss  42791  idlimc  42842  0ellimcdiv  42865  stoweidlem31  43247  stoweidlem58  43274  fourierdlem31  43354  sge0iunmpt  43631
  Copyright terms: Public domain W3C validator