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

Theorem nfne 2798
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  |-  F/_ x A
nfne.2  |-  F/_ x B
Assertion
Ref Expression
nfne  |-  F/ x  A  =/=  B

Proof of Theorem nfne
StepHypRef Expression
1 df-ne 2664 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2640 . . 3  |-  F/ x  A  =  B
54nfn 1849 . 2  |-  F/ x  -.  A  =  B
61, 5nfxfr 1625 1  |-  F/ x  A  =/=  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1379   F/wnf 1599   F/_wnfc 2615    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-nfc 2617  df-ne 2664
This theorem is referenced by:  cantnflem1  8108  ac6c4  8861  mreiincl  14851  lss1d  17409  iuncon  19723  restmetu  20853  coeeq2  22402  cvmcov  28376  fproddiv  28696  fprodn0  28714  nfwlim  28983  sltval2  29021  nobndlem5  29061  finminlem  29741  suprnmpt  31057  idlimc  31196  0ellimcdiv  31219  stoweidlem31  31359  stoweidlem58  31386  fourierdlem31  31466  iunconlem2  32833  bnj1534  33008  bnj1542  33012  bnj1398  33187  bnj1445  33197  bnj1449  33201  bnj1312  33211  bnj1525  33222  cdleme40m  35281  cdleme40n  35282  dihglblem5  36113
  Copyright terms: Public domain W3C validator