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 2958	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2937	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1877	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1873	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1560  Ⅎwnf 1803  Ⅎwnfc 2909   ≠ wne 2957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-cleq 2754  df-nfc 2911  df-ne 2958

This theorem is referenced by:  cantnflem1  9644  ac6c4  10438  fproddiv  15991  fprodn0  16009  fproddivf  16017  mreiincl  17624  lss1d  21030  iunconn  23488  restmetu  24630  coeeq2  26302  ltsval2  27720  fedgmullem2  33927  bnj1534  35148  bnj1542  35152  bnj1398  35329  bnj1445  35339  bnj1449  35343  bnj1312  35353  bnj1525  35364  cvmcov  35613  nfwlim  36170  finminlem  36678  finxpreclem2  37884  poimirlem25  38144  poimirlem26  38145  poimirlem28  38147  cdleme40m  41091  cdleme40n  41092  dihglblem5  41922  iunconnlem2  45510  eliuniin2  45698  disjf1  45761  disjrnmpt2  45766  disjinfi  45770  allbutfiinf  45994  fsumiunss  46151  idlimc  46202  0ellimcdiv  46223  stoweidlem31  46605  stoweidlem58  46632  fourierdlem31  46712  sge0iunmpt  46992