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

Theorem nfne 2774
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 2640 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2616 . . 3  |-  F/ x  A  =  B
54nfn 1887 . 2  |-  F/ x  -.  A  =  B
61, 5nfxfr 1632 1  |-  F/ x  A  =/=  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1383   F/wnf 1603   F/_wnfc 2591    =/= wne 2638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-nfc 2593  df-ne 2640
This theorem is referenced by:  cantnflem1  8111  ac6c4  8864  fproddiv  13748  fprodn0  13765  mreiincl  14975  lss1d  17588  iuncon  19907  restmetu  21068  coeeq2  22617  cvmcov  28686  nfwlim  29354  sltval2  29392  nobndlem5  29432  finminlem  30112  suprnmpt  31405  fproddivf  31542  idlimc  31586  0ellimcdiv  31609  stoweidlem31  31767  stoweidlem58  31794  fourierdlem31  31874  iunconlem2  33603  bnj1534  33779  bnj1542  33783  bnj1398  33958  bnj1445  33968  bnj1449  33972  bnj1312  33982  bnj1525  33993  cdleme40m  36068  cdleme40n  36069  dihglblem5  36900
  Copyright terms: Public domain W3C validator