Theorem nfne 2923

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 2824	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2805	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1824	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1819	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1523  Ⅎwnf 1748  Ⅎwnfc 2780   ≠ wne 2823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-nfc 2782  df-ne 2824

This theorem is referenced by:  cantnflem1  8624  ac6c4  9341  fproddiv  14735  fprodn0  14753  fproddivf  14762  mreiincl  16303  lss1d  19011  iunconn  21279  restmetu  22422  coeeq2  24043  bnj1534  31049  bnj1542  31053  bnj1398  31228  bnj1445  31238  bnj1449  31242  bnj1312  31252  bnj1525  31263  cvmcov  31371  nfwlim  31892  sltval2  31934  finminlem  32437  finxpreclem2  33357  poimirlem25  33564  poimirlem26  33565  poimirlem28  33567  cdleme40m  36072  cdleme40n  36073  dihglblem5  36904  iunconnlem2  39485  eliuniin2  39617  suprnmpt  39669  disjf1  39683  disjrnmpt2  39689  disjinfi  39694  allbutfiinf  39960  fsumiunss  40125  idlimc  40176  0ellimcdiv  40199  stoweidlem31  40566  stoweidlem58  40593  fourierdlem31  40673  sge0iunmpt  40953