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

Theorem nfne 2552
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 2461 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2439 . . 3  |-  F/ x  A  =  B
54nfn 1777 . 2  |-  F/ x  -.  A  =  B
61, 5nfxfr 1560 1  |-  F/ x  A  =/=  B
Colors of variables: wff set class
Syntax hints:   -. wn 3   F/wnf 1534    = wceq 1632   F/_wnfc 2419    =/= wne 2459
This theorem is referenced by:  ac6c4  8124  mreiincl  13514  lss1d  15736  iuncon  17170  coeeq2  19640  cvmcov  23809  sltval2  24381  nobndlem5  24421  finminlem  26334  stoweidlem31  27883  stoweidlem58  27910  bnj1534  29201  bnj1542  29205  bnj1398  29380  bnj1445  29390  bnj1449  29394  bnj1312  29404  bnj1525  29415  cdleme40m  31278  cdleme40n  31279  dihglblem5  32110
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461
  Copyright terms: Public domain W3C validator