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

Theorem nfne 2713
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 2579 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2555 . . 3  |-  F/ x  A  =  B
54nfn 1909 . 2  |-  F/ x  -.  A  =  B
61, 5nfxfr 1653 1  |-  F/ x  A  =/=  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1399   F/wnf 1624   F/_wnfc 2530    =/= wne 2577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-cleq 2374  df-nfc 2532  df-ne 2579
This theorem is referenced by:  cantnflem1  8021  ac6c4  8774  fproddiv  13768  fprodn0  13785  mreiincl  15003  lss1d  17722  iuncon  20014  restmetu  21175  coeeq2  22724  cvmcov  28897  nfwlim  29543  sltval2  29581  nobndlem5  29621  finminlem  30302  suprnmpt  31618  fproddivf  31754  idlimc  31798  0ellimcdiv  31821  stoweidlem31  31979  stoweidlem58  32006  fourierdlem31  32086  iunconlem2  34082  bnj1534  34258  bnj1542  34262  bnj1398  34437  bnj1445  34447  bnj1449  34451  bnj1312  34461  bnj1525  34472  cdleme40m  36606  cdleme40n  36607  dihglblem5  37438
  Copyright terms: Public domain W3C validator