Theorem nfne 3061

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

Step	Hyp	Ref	Expression
1		df-ne 2959	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2938	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1889	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1885	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569  Ⅎwnf 1815  Ⅎwnfc 2910   ≠ wne 2958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-cleq 2755  df-nfc 2912  df-ne 2959

This theorem is used by:  cantnflem1  9700  ac6c4  10569  fproddiv  16140  fprodn0  16158  fproddivf  16166  mreiincl  17778  lss1d  21250  iunconn  23758  restmetu  24901  coeeq2  26573  ltsval2  28025  fedgmullem2  34315  bnj1534  35536  bnj1542  35540  bnj1398  35717  bnj1445  35727  bnj1449  35731  bnj1312  35741  bnj1525  35752  cvmcov  36149  nfwlim  36711  finminlem  37233  finxpreclem2  38453  poimirlem25  38703  poimirlem26  38704  poimirlem28  38706  cdleme40m  41664  cdleme40n  41665  dihglblem5  42495  iunconnlem2  46056  eliuniin2  46274  disjf1  46337  disjrnmpt2  46342  disjinfi  46346  allbutfiinf  46569  fsumiunss  46726  idlimc  46777  0ellimcdiv  46798  stoweidlem31  47180  stoweidlem58  47207  fourierdlem31  47287  sge0iunmpt  47567