Theorem nfne 3063

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 2961	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2940	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1890	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1886	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570  Ⅎwnf 1816  Ⅎwnfc 2912   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2757  df-nfc 2914  df-ne 2961

This theorem is used by:  cantnflem1  9665  ac6c4  10480  fproddiv  16040  fprodn0  16058  fproddivf  16066  mreiincl  17672  lss1d  21136  iunconn  23637  restmetu  24780  coeeq2  26452  ltsval2  27873  fedgmullem2  34086  bnj1534  35308  bnj1542  35312  bnj1398  35489  bnj1445  35499  bnj1449  35503  bnj1312  35513  bnj1525  35524  cvmcov  35794  nfwlim  36351  finminlem  36888  finxpreclem2  38095  poimirlem25  38355  poimirlem26  38356  poimirlem28  38358  cdleme40m  41301  cdleme40n  41302  dihglblem5  42132  iunconnlem2  45703  eliuniin2  45898  disjf1  45961  disjrnmpt2  45966  disjinfi  45970  allbutfiinf  46194  fsumiunss  46351  idlimc  46402  0ellimcdiv  46423  stoweidlem31  46805  stoweidlem58  46832  fourierdlem31  46912  sge0iunmpt  47192