Theorem nfne 3033

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

Syntax hints:  ¬ wn 3   = wceq 1542  Ⅎwnf 1785  Ⅎwnfc 2883   ≠ wne 2932

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 2708

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 2728  df-nfc 2885  df-ne 2933

This theorem is referenced by:  cantnflem1  9610  ac6c4  10403  fproddiv  15926  fprodn0  15944  fproddivf  15952  mreiincl  17558  lss1d  20958  iunconn  23393  restmetu  24535  coeeq2  26207  ltsval2  27620  fedgmullem2  33774  bnj1534  34995  bnj1542  34999  bnj1398  35176  bnj1445  35186  bnj1449  35190  bnj1312  35200  bnj1525  35211  cvmcov  35445  nfwlim  36002  finminlem  36500  finxpreclem2  37706  poimirlem25  37966  poimirlem26  37967  poimirlem28  37969  cdleme40m  40913  cdleme40n  40914  dihglblem5  41744  iunconnlem2  45361  eliuniin2  45550  disjf1  45613  disjrnmpt2  45618  disjinfi  45622  allbutfiinf  45848  fsumiunss  46005  idlimc  46056  0ellimcdiv  46077  stoweidlem31  46459  stoweidlem58  46486  fourierdlem31  46566  sge0iunmpt  46846