Theorem nfne 3032

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 2932	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2911	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1856	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1852	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1539  Ⅎwnf 1782  Ⅎwnfc 2882   ≠ wne 2931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-cleq 2726  df-nfc 2884  df-ne 2932

This theorem is referenced by:  cantnflem1  9695  ac6c4  10487  fproddiv  15964  fprodn0  15982  fproddivf  15990  mreiincl  17593  lss1d  20905  iunconn  23351  restmetu  24494  coeeq2  26184  sltval2  27604  fedgmullem2  33586  bnj1534  34805  bnj1542  34809  bnj1398  34986  bnj1445  34996  bnj1449  35000  bnj1312  35010  bnj1525  35021  cvmcov  35206  nfwlim  35761  finminlem  36257  finxpreclem2  37329  poimirlem25  37590  poimirlem26  37591  poimirlem28  37593  cdleme40m  40407  cdleme40n  40408  dihglblem5  41238  iunconnlem2  44886  eliuniin2  45071  disjf1  45134  disjrnmpt2  45139  disjinfi  45143  allbutfiinf  45375  fsumiunss  45534  idlimc  45585  0ellimcdiv  45608  stoweidlem31  45990  stoweidlem58  46017  fourierdlem31  46097  sge0iunmpt  46377