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

Theorem nfne 2695
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 2601 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2579 . . 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 2559    =/= wne 2599
This theorem is referenced by:  ac6c4  8361  mreiincl  13821  lss1d  16039  iuncon  17491  restmetu  18617  coeeq2  20161  cvmcov  24950  fproddiv  25285  fprodn0  25303  nfwlim  25573  sltval2  25611  nobndlem5  25651  finminlem  26321  stoweidlem31  27756  stoweidlem58  27783  iunconlem2  29047  bnj1534  29224  bnj1542  29228  bnj1398  29403  bnj1445  29413  bnj1449  29417  bnj1312  29427  bnj1525  29438  cdleme40m  31264  cdleme40n  31265  dihglblem5  32096
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 2417
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 2429  df-clel 2432  df-nfc 2561  df-ne 2601
  Copyright terms: Public domain W3C validator