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

Syntax hints:  ¬ wn 3   = wceq 1540  Ⅎwnf 1784  Ⅎwnfc 2885   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-cleq 2729  df-nfc 2887  df-ne 2942

This theorem is referenced by:  cantnflem1  9518  ac6c4  10310  fproddiv  15743  fprodn0  15761  fproddivf  15769  mreiincl  17375  lss1d  20297  iunconn  22651  restmetu  23798  coeeq2  25475  sltval2  26876  fedgmullem2  31817  bnj1534  32938  bnj1542  32942  bnj1398  33119  bnj1445  33129  bnj1449  33133  bnj1312  33143  bnj1525  33154  cvmcov  33330  nfwlim  33911  finminlem  34565  finxpreclem2  35617  poimirlem25  35858  poimirlem26  35859  poimirlem28  35861  cdleme40m  38686  cdleme40n  38687  dihglblem5  39517  iunconnlem2  42776  eliuniin2  42891  disjf1  42948  disjrnmpt2  42954  disjinfi  42959  allbutfiinf  43196  fsumiunss  43353  idlimc  43404  0ellimcdiv  43427  stoweidlem31  43809  stoweidlem58  43836  fourierdlem31  43916  sge0iunmpt  44194