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

Theorem nfne 2757
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 2621 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 nfne.1 . . . 4  |-  F/_ x A
3 nfne.2 . . . 4  |-  F/_ x B
42, 3nfeq 2596 . . 3  |-  F/ x  A  =  B
54nfn 1957 . 2  |-  F/ x  -.  A  =  B
61, 5nfxfr 1693 1  |-  F/ x  A  =/=  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1438   F/wnf 1664   F/_wnfc 2571    =/= wne 2619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-cleq 2415  df-nfc 2573  df-ne 2621
This theorem is referenced by:  cantnflem1  8201  ac6c4  8917  fproddiv  14012  fprodn0  14030  fproddivf  14038  mreiincl  15499  lss1d  18183  iuncon  20439  restmetu  21581  coeeq2  23192  bnj1534  29670  bnj1542  29674  bnj1398  29849  bnj1445  29859  bnj1449  29863  bnj1312  29873  bnj1525  29884  cvmcov  29992  nfwlim  30510  sltval2  30548  nobndlem5  30588  finminlem  30977  finxpreclem2  31744  poimirlem25  31927  poimirlem26  31928  poimirlem28  31930  cdleme40m  34001  cdleme40n  34002  dihglblem5  34833  iunconlem2  37241  suprnmpt  37336  disjf1  37355  disjrnmpt2  37361  disjinfi  37366  fsumiunss  37525  idlimc  37574  0ellimcdiv  37598  stoweidlem31  37760  stoweidlem58  37787  fourierdlem31  37868  fourierdlem31OLD  37869  sge0iunmpt  38096
  Copyright terms: Public domain W3C validator