Theorem nfne 3029

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 2929	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2908	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1858	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1854	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1541  Ⅎwnf 1784  Ⅎwnfc 2879   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2723  df-nfc 2881  df-ne 2929

This theorem is referenced by:  cantnflem1  9579  ac6c4  10372  fproddiv  15868  fprodn0  15886  fproddivf  15894  mreiincl  17498  lss1d  20896  iunconn  23343  restmetu  24485  coeeq2  26174  sltval2  27595  fedgmullem2  33643  bnj1534  34865  bnj1542  34869  bnj1398  35046  bnj1445  35056  bnj1449  35060  bnj1312  35070  bnj1525  35081  cvmcov  35307  nfwlim  35864  finminlem  36362  finxpreclem2  37434  poimirlem25  37695  poimirlem26  37696  poimirlem28  37698  cdleme40m  40576  cdleme40n  40577  dihglblem5  41407  iunconnlem2  45037  eliuniin2  45227  disjf1  45290  disjrnmpt2  45295  disjinfi  45299  allbutfiinf  45528  fsumiunss  45685  idlimc  45736  0ellimcdiv  45757  stoweidlem31  46139  stoweidlem58  46166  fourierdlem31  46246  sge0iunmpt  46526