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

Syntax hints:  ¬ wn 3   = wceq 1542  Ⅎwnf 1786  Ⅎwnfc 2884   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-nfc 2886  df-ne 2942

This theorem is referenced by:  cantnflem1  9684  ac6c4  10476  fproddiv  15905  fprodn0  15923  fproddivf  15931  mreiincl  17540  lss1d  20574  iunconn  22932  restmetu  24079  coeeq2  25756  sltval2  27159  fedgmullem2  32715  bnj1534  33864  bnj1542  33868  bnj1398  34045  bnj1445  34055  bnj1449  34059  bnj1312  34069  bnj1525  34080  cvmcov  34254  nfwlim  34794  finminlem  35203  finxpreclem2  36271  poimirlem25  36513  poimirlem26  36514  poimirlem28  36516  cdleme40m  39338  cdleme40n  39339  dihglblem5  40169  iunconnlem2  43696  eliuniin2  43809  disjf1  43880  disjrnmpt2  43886  disjinfi  43891  allbutfiinf  44130  fsumiunss  44291  idlimc  44342  0ellimcdiv  44365  stoweidlem31  44747  stoweidlem58  44774  fourierdlem31  44854  sge0iunmpt  45134