Theorem nfne 3034

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 2934	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2913	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1859	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1855	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1542  Ⅎwnf 1785  Ⅎwnfc 2884   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-nfc 2886  df-ne 2934

This theorem is referenced by:  cantnflem1  9604  ac6c4  10397  fproddiv  15920  fprodn0  15938  fproddivf  15946  mreiincl  17552  lss1d  20952  iunconn  23406  restmetu  24548  coeeq2  26220  ltsval2  27637  fedgmullem2  33793  bnj1534  35014  bnj1542  35018  bnj1398  35195  bnj1445  35205  bnj1449  35209  bnj1312  35219  bnj1525  35230  cvmcov  35464  nfwlim  36021  finminlem  36519  finxpreclem2  37723  poimirlem25  37983  poimirlem26  37984  poimirlem28  37986  cdleme40m  40930  cdleme40n  40931  dihglblem5  41761  iunconnlem2  45382  eliuniin2  45571  disjf1  45634  disjrnmpt2  45639  disjinfi  45643  allbutfiinf  45869  fsumiunss  46026  idlimc  46077  0ellimcdiv  46098  stoweidlem31  46480  stoweidlem58  46507  fourierdlem31  46587  sge0iunmpt  46867