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

Theorem nfne 2539
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 2448 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2426 . . 3  |-  F/ x  A  =  B
54nfn 1765 . 2  |-  F/ x  -.  A  =  B
61, 5nfxfr 1557 1  |-  F/ x  A  =/=  B
Colors of variables: wff set class
Syntax hints:   -. wn 3   F/wnf 1531    = wceq 1623   F/_wnfc 2406    =/= wne 2446
This theorem is referenced by:  ac6c4  8108  mreiincl  13498  lss1d  15720  iuncon  17154  coeeq2  19624  cvmcov  23794  sltval2  24310  nobndlem5  24350  finminlem  26231  stoweidlem31  27780  stoweidlem58  27807  bnj1534  28885  bnj1542  28889  bnj1398  29064  bnj1445  29074  bnj1449  29078  bnj1312  29088  bnj1525  29099  cdleme40m  30656  cdleme40n  30657  dihglblem5  31488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448
  Copyright terms: Public domain W3C validator