Theorem nfne 3044

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 2943	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2919	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1861	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1856	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1539  Ⅎwnf 1787  Ⅎwnfc 2886   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-cleq 2730  df-nfc 2888  df-ne 2943

This theorem is referenced by:  cantnflem1  9377  ac6c4  10168  fproddiv  15599  fprodn0  15617  fproddivf  15625  mreiincl  17222  lss1d  20140  iunconn  22487  restmetu  23632  coeeq2  25308  fedgmullem2  31613  bnj1534  32733  bnj1542  32737  bnj1398  32914  bnj1445  32924  bnj1449  32928  bnj1312  32938  bnj1525  32949  cvmcov  33125  nfwlim  33743  sltval2  33786  finminlem  34434  finxpreclem2  35488  poimirlem25  35729  poimirlem26  35730  poimirlem28  35732  cdleme40m  38408  cdleme40n  38409  dihglblem5  39239  iunconnlem2  42444  eliuniin2  42558  disjf1  42609  disjrnmpt2  42615  disjinfi  42620  allbutfiinf  42850  fsumiunss  43006  idlimc  43057  0ellimcdiv  43080  stoweidlem31  43462  stoweidlem58  43489  fourierdlem31  43569  sge0iunmpt  43846