Theorem nfne 3089

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 2987	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2962	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1842	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1838	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1525  Ⅎwnf 1769  Ⅎwnfc 2935   ≠ wne 2986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-cleq 2790  df-nfc 2937  df-ne 2987

This theorem is referenced by:  cantnflem1  9005  ac6c4  9756  fproddiv  15152  fprodn0  15170  fproddivf  15178  mreiincl  16700  lss1d  19429  iunconn  21724  restmetu  22867  coeeq2  24519  fedgmullem2  30626  bnj1534  31737  bnj1542  31741  bnj1398  31916  bnj1445  31926  bnj1449  31930  bnj1312  31940  bnj1525  31951  cvmcov  32120  nfwlim  32720  sltval2  32774  finminlem  33277  finxpreclem2  34223  poimirlem25  34469  poimirlem26  34470  poimirlem28  34472  cdleme40m  37155  cdleme40n  37156  dihglblem5  37986  iunconnlem2  40829  eliuniin2  40947  suprnmpt  40991  disjf1  41004  disjrnmpt2  41010  disjinfi  41015  allbutfiinf  41257  fsumiunss  41419  idlimc  41470  0ellimcdiv  41493  stoweidlem31  41880  stoweidlem58  41907  fourierdlem31  41987  sge0iunmpt  42264