Theorem nfne 3026

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 2926	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2905	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1853	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2876   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-nfc 2878  df-ne 2926

This theorem is referenced by:  cantnflem1  9585  ac6c4  10375  fproddiv  15868  fprodn0  15886  fproddivf  15894  mreiincl  17498  lss1d  20866  iunconn  23313  restmetu  24456  coeeq2  26145  sltval2  27566  fedgmullem2  33603  bnj1534  34826  bnj1542  34830  bnj1398  35007  bnj1445  35017  bnj1449  35021  bnj1312  35031  bnj1525  35042  cvmcov  35246  nfwlim  35806  finminlem  36302  finxpreclem2  37374  poimirlem25  37635  poimirlem26  37636  poimirlem28  37638  cdleme40m  40456  cdleme40n  40457  dihglblem5  41287  iunconnlem2  44918  eliuniin2  45108  disjf1  45171  disjrnmpt2  45176  disjinfi  45180  allbutfiinf  45409  fsumiunss  45566  idlimc  45617  0ellimcdiv  45640  stoweidlem31  46022  stoweidlem58  46049  fourierdlem31  46129  sge0iunmpt  46409