Theorem nfne 3043

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

Syntax hints:  ¬ wn 3   = wceq 1541  Ⅎwnf 1785  Ⅎwnfc 2883   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-cleq 2724  df-nfc 2885  df-ne 2941

This theorem is referenced by:  cantnflem1  9683  ac6c4  10475  fproddiv  15904  fprodn0  15922  fproddivf  15930  mreiincl  17539  lss1d  20573  iunconn  22931  restmetu  24078  coeeq2  25755  sltval2  27156  fedgmullem2  32710  bnj1534  33859  bnj1542  33863  bnj1398  34040  bnj1445  34050  bnj1449  34054  bnj1312  34064  bnj1525  34075  cvmcov  34249  nfwlim  34789  finminlem  35198  finxpreclem2  36266  poimirlem25  36508  poimirlem26  36509  poimirlem28  36511  cdleme40m  39333  cdleme40n  39334  dihglblem5  40164  iunconnlem2  43686  eliuniin2  43799  disjf1  43870  disjrnmpt2  43876  disjinfi  43881  allbutfiinf  44120  fsumiunss  44281  idlimc  44332  0ellimcdiv  44355  stoweidlem31  44737  stoweidlem58  44764  fourierdlem31  44844  sge0iunmpt  45124