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

Theorem nfne 2689
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 2600 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2578 . . 3  |-  F/ x  A  =  B
54nfn 1811 . 2  |-  F/ x  -.  A  =  B
61, 5nfxfr 1579 1  |-  F/ x  A  =/=  B
Colors of variables: wff set class
Syntax hints:   -. wn 3   F/wnf 1553    = wceq 1652   F/_wnfc 2558    =/= wne 2598
This theorem is referenced by:  ac6c4  8353  mreiincl  13813  lss1d  16031  iuncon  17483  restmetu  18609  coeeq2  20153  cvmcov  24942  fproddiv  25277  fprodn0  25295  nfwlim  25565  sltval2  25603  nobndlem5  25643  finminlem  26302  stoweidlem31  27737  stoweidlem58  27764  iunconlem2  28974  bnj1534  29151  bnj1542  29155  bnj1398  29330  bnj1445  29340  bnj1449  29344  bnj1312  29354  bnj1525  29365  cdleme40m  31191  cdleme40n  31192  dihglblem5  32023
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600
  Copyright terms: Public domain W3C validator