Theorem nfne 2882

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 2782	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2762	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1768	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1771	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1475  Ⅎwnf 1699  Ⅎwnfc 2738   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-nfc 2740  df-ne 2782

This theorem is referenced by:  cantnflem1  8469  ac6c4  9186  fproddiv  14530  fprodn0  14548  fproddivf  14557  mreiincl  16079  lss1d  18784  iuncon  21041  restmetu  22185  coeeq2  23802  bnj1534  30177  bnj1542  30181  bnj1398  30356  bnj1445  30366  bnj1449  30370  bnj1312  30380  bnj1525  30391  cvmcov  30499  nfwlim  31012  sltval2  31053  nobndlem5  31095  finminlem  31482  finxpreclem2  32403  poimirlem25  32604  poimirlem26  32605  poimirlem28  32607  cdleme40m  34773  cdleme40n  34774  dihglblem5  35605  iunconlem2  38193  eliuniin2  38335  suprnmpt  38350  disjf1  38364  disjrnmpt2  38370  disjinfi  38375  fsumiunss  38642  idlimc  38693  0ellimcdiv  38716  stoweidlem31  38924  stoweidlem58  38951  fourierdlem31  39031  sge0iunmpt  39311