Theorem nfne 3045

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

Syntax hints:  ¬ wn 3   = wceq 1539  Ⅎwnf 1786  Ⅎwnfc 2887   ≠ wne 2943

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-cleq 2730  df-nfc 2889  df-ne 2944

This theorem is referenced by:  cantnflem1  9447  ac6c4  10237  fproddiv  15671  fprodn0  15689  fproddivf  15697  mreiincl  17305  lss1d  20225  iunconn  22579  restmetu  23726  coeeq2  25403  fedgmullem2  31711  bnj1534  32833  bnj1542  32837  bnj1398  33014  bnj1445  33024  bnj1449  33028  bnj1312  33038  bnj1525  33049  cvmcov  33225  nfwlim  33816  sltval2  33859  finminlem  34507  finxpreclem2  35561  poimirlem25  35802  poimirlem26  35803  poimirlem28  35805  cdleme40m  38481  cdleme40n  38482  dihglblem5  39312  iunconnlem2  42555  eliuniin2  42669  disjf1  42720  disjrnmpt2  42726  disjinfi  42731  allbutfiinf  42960  fsumiunss  43116  idlimc  43167  0ellimcdiv  43190  stoweidlem31  43572  stoweidlem58  43599  fourierdlem31  43679  sge0iunmpt  43956