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  9642  ac6c4  10434  fproddiv  15927  fprodn0  15945  fproddivf  15953  mreiincl  17557  lss1d  20869  iunconn  23315  restmetu  24458  coeeq2  26147  sltval2  27568  fedgmullem2  33626  bnj1534  34843  bnj1542  34847  bnj1398  35024  bnj1445  35034  bnj1449  35038  bnj1312  35048  bnj1525  35059  cvmcov  35250  nfwlim  35810  finminlem  36306  finxpreclem2  37378  poimirlem25  37639  poimirlem26  37640  poimirlem28  37642  cdleme40m  40461  cdleme40n  40462  dihglblem5  41292  iunconnlem2  44924  eliuniin2  45114  disjf1  45177  disjrnmpt2  45182  disjinfi  45186  allbutfiinf  45416  fsumiunss  45573  idlimc  45624  0ellimcdiv  45647  stoweidlem31  46029  stoweidlem58  46056  fourierdlem31  46136  sge0iunmpt  46416