Theorem nfne 3059

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 2957	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2936	. . 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 2908   ≠ wne 2956

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 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

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 2753  df-nfc 2910  df-ne 2957

This theorem is used by:  cantnflem1  9690  ac6c4  10559  fproddiv  16128  fprodn0  16146  fproddivf  16154  mreiincl  17766  lss1d  21238  iunconn  23746  restmetu  24889  coeeq2  26561  ltsval2  28013  fedgmullem2  34262  bnj1534  35483  bnj1542  35487  bnj1398  35664  bnj1445  35674  bnj1449  35678  bnj1312  35688  bnj1525  35699  cvmcov  36028  nfwlim  36584  finminlem  37106  finxpreclem2  38313  poimirlem25  38563  poimirlem26  38564  poimirlem28  38566  cdleme40m  41524  cdleme40n  41525  dihglblem5  42355  iunconnlem2  45916  eliuniin2  46134  disjf1  46197  disjrnmpt2  46202  disjinfi  46206  allbutfiinf  46429  fsumiunss  46586  idlimc  46637  0ellimcdiv  46658  stoweidlem31  47040  stoweidlem58  47067  fourierdlem31  47147  sge0iunmpt  47427