Theorem nfne 3048

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 2948	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2927	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1867	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1863	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1550  Ⅎwnf 1793  Ⅎwnfc 2899   ≠ wne 2947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1553  df-ex 1790  df-nf 1794  df-cleq 2744  df-nfc 2901  df-ne 2948

This theorem is referenced by:  cantnflem1  9630  ac6c4  10424  fproddiv  15963  fprodn0  15981  fproddivf  15989  mreiincl  17596  lss1d  20999  iunconn  23457  restmetu  24599  coeeq2  26271  ltsval2  27686  fedgmullem2  33871  bnj1534  35095  bnj1542  35099  bnj1398  35276  bnj1445  35286  bnj1449  35290  bnj1312  35300  bnj1525  35311  cvmcov  35551  nfwlim  36108  finminlem  36616  finxpreclem2  37822  poimirlem25  38082  poimirlem26  38083  poimirlem28  38085  cdleme40m  41029  cdleme40n  41030  dihglblem5  41860  iunconnlem2  45448  eliuniin2  45636  disjf1  45699  disjrnmpt2  45704  disjinfi  45708  allbutfiinf  45932  fsumiunss  46089  idlimc  46140  0ellimcdiv  46161  stoweidlem31  46543  stoweidlem58  46570  fourierdlem31  46650  sge0iunmpt  46930