Theorem nfne 3040

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 2938	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2916	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1854	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1849	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1536  Ⅎwnf 1779  Ⅎwnfc 2887   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-cleq 2726  df-nfc 2889  df-ne 2938

This theorem is referenced by:  cantnflem1  9726  ac6c4  10518  fproddiv  15993  fprodn0  16011  fproddivf  16019  mreiincl  17640  lss1d  20978  iunconn  23451  restmetu  24598  coeeq2  26295  sltval2  27715  fedgmullem2  33657  bnj1534  34845  bnj1542  34849  bnj1398  35026  bnj1445  35036  bnj1449  35040  bnj1312  35050  bnj1525  35061  cvmcov  35247  nfwlim  35803  finminlem  36300  finxpreclem2  37372  poimirlem25  37631  poimirlem26  37632  poimirlem28  37634  cdleme40m  40449  cdleme40n  40450  dihglblem5  41280  iunconnlem2  44932  eliuniin2  45059  disjf1  45125  disjrnmpt2  45130  disjinfi  45134  allbutfiinf  45369  fsumiunss  45530  idlimc  45581  0ellimcdiv  45604  stoweidlem31  45986  stoweidlem58  46013  fourierdlem31  46093  sge0iunmpt  46373