Theorem nfne 3033

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 2933	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2912	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1857	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1853	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2883   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2727  df-nfc 2885  df-ne 2933

This theorem is referenced by:  cantnflem1  9701  ac6c4  10493  fproddiv  15975  fprodn0  15993  fproddivf  16001  mreiincl  17606  lss1d  20918  iunconn  23364  restmetu  24507  coeeq2  26197  sltval2  27618  fedgmullem2  33616  bnj1534  34830  bnj1542  34834  bnj1398  35011  bnj1445  35021  bnj1449  35025  bnj1312  35035  bnj1525  35046  cvmcov  35231  nfwlim  35786  finminlem  36282  finxpreclem2  37354  poimirlem25  37615  poimirlem26  37616  poimirlem28  37618  cdleme40m  40432  cdleme40n  40433  dihglblem5  41263  iunconnlem2  44907  eliuniin2  45092  disjf1  45155  disjrnmpt2  45160  disjinfi  45164  allbutfiinf  45395  fsumiunss  45552  idlimc  45603  0ellimcdiv  45626  stoweidlem31  46008  stoweidlem58  46035  fourierdlem31  46115  sge0iunmpt  46395