Theorem nfne 3027

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 2927	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2906	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1853	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2877   ≠ wne 2926

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 2702

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 2722  df-nfc 2879  df-ne 2927

This theorem is referenced by:  cantnflem1  9649  ac6c4  10441  fproddiv  15934  fprodn0  15952  fproddivf  15960  mreiincl  17564  lss1d  20876  iunconn  23322  restmetu  24465  coeeq2  26154  sltval2  27575  fedgmullem2  33633  bnj1534  34850  bnj1542  34854  bnj1398  35031  bnj1445  35041  bnj1449  35045  bnj1312  35055  bnj1525  35066  cvmcov  35257  nfwlim  35817  finminlem  36313  finxpreclem2  37385  poimirlem25  37646  poimirlem26  37647  poimirlem28  37649  cdleme40m  40468  cdleme40n  40469  dihglblem5  41299  iunconnlem2  44931  eliuniin2  45121  disjf1  45184  disjrnmpt2  45189  disjinfi  45193  allbutfiinf  45423  fsumiunss  45580  idlimc  45631  0ellimcdiv  45654  stoweidlem31  46036  stoweidlem58  46063  fourierdlem31  46143  sge0iunmpt  46423