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

Theorem nfne 2708
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 2613 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2591 . . 3  |-  F/ x  A  =  B
54nfn 1835 . 2  |-  F/ x  -.  A  =  B
61, 5nfxfr 1615 1  |-  F/ x  A  =/=  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1369   F/wnf 1589   F/_wnfc 2571    =/= wne 2611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613
This theorem is referenced by:  cantnflem1  7902  ac6c4  8655  mreiincl  14539  lss1d  17049  iuncon  19037  restmetu  20167  coeeq2  21715  cvmcov  27157  fproddiv  27477  fprodn0  27495  nfwlim  27764  sltval2  27802  nobndlem5  27842  finminlem  28518  stoweidlem31  29831  stoweidlem58  29858  iunconlem2  31676  bnj1534  31851  bnj1542  31855  bnj1398  32030  bnj1445  32040  bnj1449  32044  bnj1312  32054  bnj1525  32065  cdleme40m  34116  cdleme40n  34117  dihglblem5  34948
  Copyright terms: Public domain W3C validator