Theorem nfne 3035

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

Syntax hints:  ¬ wn 3   = wceq 1547  Ⅎwnf 1790  Ⅎwnfc 2886   ≠ wne 2934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-cleq 2731  df-nfc 2888  df-ne 2935

This theorem is referenced by:  cantnflem1  9601  ac6c4  10394  fproddiv  15917  fprodn0  15935  fproddivf  15943  mreiincl  17549  lss1d  20953  iunconn  23411  restmetu  24553  coeeq2  26225  ltsval2  27638  fedgmullem2  33814  bnj1534  35035  bnj1542  35039  bnj1398  35216  bnj1445  35226  bnj1449  35230  bnj1312  35240  bnj1525  35251  cvmcov  35491  nfwlim  36048  finminlem  36546  finxpreclem2  37752  poimirlem25  38012  poimirlem26  38013  poimirlem28  38015  cdleme40m  40959  cdleme40n  40960  dihglblem5  41790  iunconnlem2  45378  eliuniin2  45567  disjf1  45630  disjrnmpt2  45635  disjinfi  45639  allbutfiinf  45863  fsumiunss  46020  idlimc  46071  0ellimcdiv  46092  stoweidlem31  46474  stoweidlem58  46501  fourierdlem31  46581  sge0iunmpt  46861