Theorem nfne 3031

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

Syntax hints:  ¬ wn 3   = wceq 1541  Ⅎwnf 1784  Ⅎwnfc 2881   ≠ wne 2930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2726  df-nfc 2883  df-ne 2931

This theorem is referenced by:  cantnflem1  9596  ac6c4  10389  fproddiv  15882  fprodn0  15900  fproddivf  15908  mreiincl  17513  lss1d  20912  iunconn  23370  restmetu  24512  coeeq2  26201  sltval2  27622  fedgmullem2  33736  bnj1534  34958  bnj1542  34962  bnj1398  35139  bnj1445  35149  bnj1449  35153  bnj1312  35163  bnj1525  35174  cvmcov  35406  nfwlim  35963  finminlem  36461  finxpreclem2  37534  poimirlem25  37785  poimirlem26  37786  poimirlem28  37788  cdleme40m  40666  cdleme40n  40667  dihglblem5  41497  iunconnlem2  45117  eliuniin2  45306  disjf1  45369  disjrnmpt2  45374  disjinfi  45378  allbutfiinf  45606  fsumiunss  45763  idlimc  45814  0ellimcdiv  45835  stoweidlem31  46217  stoweidlem58  46244  fourierdlem31  46324  sge0iunmpt  46604