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 1887	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1883	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1570  Ⅎwnf 1813  Ⅎwnfc 2910   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-cleq 2755  df-nfc 2912  df-ne 2959

This theorem is referenced by:  cantnflem1  9654  ac6c4  10460  fproddiv  16011  fprodn0  16029  fproddivf  16037  mreiincl  17643  lss1d  21084  iunconn  23585  restmetu  24727  coeeq2  26399  ltsval2  27820  fedgmullem2  34020  bnj1534  35241  bnj1542  35245  bnj1398  35422  bnj1445  35432  bnj1449  35436  bnj1312  35446  bnj1525  35457  cvmcov  35755  nfwlim  36312  finminlem  36849  finxpreclem2  38056  poimirlem25  38316  poimirlem26  38317  poimirlem28  38319  cdleme40m  41261  cdleme40n  41262  dihglblem5  42092  iunconnlem2  45663  eliuniin2  45858  disjf1  45921  disjrnmpt2  45926  disjinfi  45930  allbutfiinf  46154  fsumiunss  46311  idlimc  46362  0ellimcdiv  46383  stoweidlem31  46765  stoweidlem58  46792  fourierdlem31  46872  sge0iunmpt  47152