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

Theorem nfne 2878
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 𝑥𝐴
nfne.2 𝑥𝐵
Assertion
Ref Expression
nfne 𝑥 𝐴𝐵

Proof of Theorem nfne
StepHypRef Expression
1 df-ne 2778 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 nfne.1 . . . 4 𝑥𝐴
3 nfne.2 . . . 4 𝑥𝐵
42, 3nfeq 2758 . . 3 𝑥 𝐴 = 𝐵
54nfn 1767 . 2 𝑥 ¬ 𝐴 = 𝐵
61, 5nfxfr 1770 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1474  wnf 1698  wnfc 2734  wne 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2599  df-nfc 2736  df-ne 2778
This theorem is referenced by:  cantnflem1  8443  ac6c4  9160  fproddiv  14473  fprodn0  14491  fproddivf  14500  mreiincl  16022  lss1d  18727  iuncon  20980  restmetu  22123  coeeq2  23716  bnj1534  29980  bnj1542  29984  bnj1398  30159  bnj1445  30169  bnj1449  30173  bnj1312  30183  bnj1525  30194  cvmcov  30302  nfwlim  30815  sltval2  30856  nobndlem5  30898  finminlem  31285  finxpreclem2  32203  poimirlem25  32404  poimirlem26  32405  poimirlem28  32407  cdleme40m  34573  cdleme40n  34574  dihglblem5  35405  iunconlem2  37993  eliuniin2  38135  suprnmpt  38150  disjf1  38164  disjrnmpt2  38170  disjinfi  38175  fsumiunss  38443  idlimc  38494  0ellimcdiv  38517  stoweidlem31  38725  stoweidlem58  38752  fourierdlem31  38832  sge0iunmpt  39112
  Copyright terms: Public domain W3C validator