Theorem nfne 3042

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 2941	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2917	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1865	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1860	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1543  Ⅎwnf 1791  Ⅎwnfc 2884   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-cleq 2729  df-nfc 2886  df-ne 2941

This theorem is referenced by:  cantnflem1  9304  ac6c4  10095  fproddiv  15523  fprodn0  15541  fproddivf  15549  mreiincl  17099  lss1d  20000  iunconn  22325  restmetu  23468  coeeq2  25136  fedgmullem2  31425  bnj1534  32546  bnj1542  32550  bnj1398  32727  bnj1445  32737  bnj1449  32741  bnj1312  32751  bnj1525  32762  cvmcov  32938  nfwlim  33553  sltval2  33596  finminlem  34244  finxpreclem2  35298  poimirlem25  35539  poimirlem26  35540  poimirlem28  35542  cdleme40m  38218  cdleme40n  38219  dihglblem5  39049  iunconnlem2  42228  eliuniin2  42342  disjf1  42393  disjrnmpt2  42399  disjinfi  42404  allbutfiinf  42633  fsumiunss  42791  idlimc  42842  0ellimcdiv  42865  stoweidlem31  43247  stoweidlem58  43274  fourierdlem31  43354  sge0iunmpt  43631