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 1858	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1854	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1541  Ⅎwnf 1784  Ⅎwnfc 2883   ≠ wne 2932

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 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2728  df-nfc 2885  df-ne 2933

This theorem is referenced by:  cantnflem1  9598  ac6c4  10391  fproddiv  15884  fprodn0  15902  fproddivf  15910  mreiincl  17515  lss1d  20914  iunconn  23372  restmetu  24514  coeeq2  26203  ltsval2  27624  fedgmullem2  33787  bnj1534  35009  bnj1542  35013  bnj1398  35190  bnj1445  35200  bnj1449  35204  bnj1312  35214  bnj1525  35225  cvmcov  35457  nfwlim  36014  finminlem  36512  finxpreclem2  37595  poimirlem25  37846  poimirlem26  37847  poimirlem28  37849  cdleme40m  40737  cdleme40n  40738  dihglblem5  41568  iunconnlem2  45185  eliuniin2  45374  disjf1  45437  disjrnmpt2  45442  disjinfi  45446  allbutfiinf  45674  fsumiunss  45831  idlimc  45882  0ellimcdiv  45903  stoweidlem31  46285  stoweidlem58  46312  fourierdlem31  46392  sge0iunmpt  46672