Theorem nfne 2894

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 2795	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2776	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1784	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1779	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1483  Ⅎwnf 1708  Ⅎwnfc 2751   ≠ wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-nfc 2753  df-ne 2795

This theorem is referenced by:  cantnflem1  8586  ac6c4  9303  fproddiv  14691  fprodn0  14709  fproddivf  14718  mreiincl  16256  lss1d  18963  iunconn  21231  restmetu  22375  coeeq2  23998  bnj1534  30923  bnj1542  30927  bnj1398  31102  bnj1445  31112  bnj1449  31116  bnj1312  31126  bnj1525  31137  cvmcov  31245  nfwlim  31768  sltval2  31809  finminlem  32312  finxpreclem2  33227  poimirlem25  33434  poimirlem26  33435  poimirlem28  33437  cdleme40m  35755  cdleme40n  35756  dihglblem5  36587  iunconnlem2  39171  eliuniin2  39303  suprnmpt  39355  disjf1  39369  disjrnmpt2  39375  disjinfi  39380  allbutfiinf  39647  fsumiunss  39807  idlimc  39858  0ellimcdiv  39881  stoweidlem31  40248  stoweidlem58  40275  fourierdlem31  40355  sge0iunmpt  40635