Theorem nfne 3067

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 2965	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2944	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1884	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1880	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1567  Ⅎwnf 1810  Ⅎwnfc 2916   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-cleq 2761  df-nfc 2918  df-ne 2965

This theorem is referenced by:  cantnflem1  9658  ac6c4  10465  fproddiv  16015  fprodn0  16033  fproddivf  16041  mreiincl  17648  lss1d  21062  iunconn  23554  restmetu  24696  coeeq2  26368  ltsval2  27786  fedgmullem2  33965  bnj1534  35186  bnj1542  35190  bnj1398  35367  bnj1445  35377  bnj1449  35381  bnj1312  35391  bnj1525  35402  cvmcov  35654  nfwlim  36211  finminlem  36718  finxpreclem2  37924  poimirlem25  38184  poimirlem26  38185  poimirlem28  38187  cdleme40m  41131  cdleme40n  41132  dihglblem5  41962  iunconnlem2  45535  eliuniin2  45730  disjf1  45793  disjrnmpt2  45798  disjinfi  45802  allbutfiinf  46026  fsumiunss  46183  idlimc  46234  0ellimcdiv  46255  stoweidlem31  46637  stoweidlem58  46664  fourierdlem31  46744  sge0iunmpt  47024