Theorem nfne 3034

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

Syntax hints:  ¬ wn 3   = wceq 1542  Ⅎwnf 1785  Ⅎwnfc 2884   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-nfc 2886  df-ne 2934

This theorem is referenced by:  cantnflem1  9610  ac6c4  10403  fproddiv  15896  fprodn0  15914  fproddivf  15922  mreiincl  17527  lss1d  20929  iunconn  23387  restmetu  24529  coeeq2  26218  ltsval2  27639  fedgmullem2  33812  bnj1534  35033  bnj1542  35037  bnj1398  35214  bnj1445  35224  bnj1449  35228  bnj1312  35238  bnj1525  35249  cvmcov  35483  nfwlim  36040  finminlem  36538  finxpreclem2  37649  poimirlem25  37900  poimirlem26  37901  poimirlem28  37903  cdleme40m  40847  cdleme40n  40848  dihglblem5  41678  iunconnlem2  45294  eliuniin2  45483  disjf1  45546  disjrnmpt2  45551  disjinfi  45555  allbutfiinf  45782  fsumiunss  45939  idlimc  45990  0ellimcdiv  46011  stoweidlem31  46393  stoweidlem58  46420  fourierdlem31  46500  sge0iunmpt  46780