Theorem nfne 3058

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 2956	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2935	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1890	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1886	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570  Ⅎwnf 1816  Ⅎwnfc 2907   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2752  df-nfc 2909  df-ne 2956

This theorem is used by:  cantnflem1  9671  ac6c4  10486  fproddiv  16051  fprodn0  16069  fproddivf  16077  mreiincl  17683  lss1d  21150  iunconn  23656  restmetu  24799  coeeq2  26471  ltsval2  27895  fedgmullem2  34143  bnj1534  35365  bnj1542  35369  bnj1398  35546  bnj1445  35556  bnj1449  35560  bnj1312  35570  bnj1525  35581  cvmcov  35845  nfwlim  36402  finminlem  36940  finxpreclem2  38147  poimirlem25  38397  poimirlem26  38398  poimirlem28  38400  cdleme40m  41343  cdleme40n  41344  dihglblem5  42174  iunconnlem2  45760  eliuniin2  45955  disjf1  46018  disjrnmpt2  46023  disjinfi  46027  allbutfiinf  46251  fsumiunss  46408  idlimc  46459  0ellimcdiv  46480  stoweidlem31  46862  stoweidlem58  46889  fourierdlem31  46969  sge0iunmpt  47249