Theorem nfne 3043

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

Syntax hints:  ¬ wn 3   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2890   ≠ wne 2940

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 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-nfc 2892  df-ne 2941

This theorem is referenced by:  cantnflem1  9729  ac6c4  10521  fproddiv  15997  fprodn0  16015  fproddivf  16023  mreiincl  17639  lss1d  20961  iunconn  23436  restmetu  24583  coeeq2  26281  sltval2  27701  fedgmullem2  33681  bnj1534  34867  bnj1542  34871  bnj1398  35048  bnj1445  35058  bnj1449  35062  bnj1312  35072  bnj1525  35083  cvmcov  35268  nfwlim  35823  finminlem  36319  finxpreclem2  37391  poimirlem25  37652  poimirlem26  37653  poimirlem28  37655  cdleme40m  40469  cdleme40n  40470  dihglblem5  41300  iunconnlem2  44955  eliuniin2  45125  disjf1  45188  disjrnmpt2  45193  disjinfi  45197  allbutfiinf  45431  fsumiunss  45590  idlimc  45641  0ellimcdiv  45664  stoweidlem31  46046  stoweidlem58  46073  fourierdlem31  46153  sge0iunmpt  46433