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  9618  ac6c4  10410  fproddiv  15903  fprodn0  15921  fproddivf  15929  mreiincl  17533  lss1d  20901  iunconn  23348  restmetu  24491  coeeq2  26180  sltval2  27601  fedgmullem2  33619  bnj1534  34836  bnj1542  34840  bnj1398  35017  bnj1445  35027  bnj1449  35031  bnj1312  35041  bnj1525  35052  cvmcov  35243  nfwlim  35803  finminlem  36299  finxpreclem2  37371  poimirlem25  37632  poimirlem26  37633  poimirlem28  37635  cdleme40m  40454  cdleme40n  40455  dihglblem5  41285  iunconnlem2  44917  eliuniin2  45107  disjf1  45170  disjrnmpt2  45175  disjinfi  45179  allbutfiinf  45409  fsumiunss  45566  idlimc  45617  0ellimcdiv  45640  stoweidlem31  46022  stoweidlem58  46049  fourierdlem31  46129  sge0iunmpt  46409