Theorem nfne 3049

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 2947	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		nfne.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfne.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	2, 3	nfeq 2922	. . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵
5	4	nfn 1856	. 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵
6	1, 5	nfxfr 1851	1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵

Syntax hints:  ¬ wn 3   = wceq 1537  Ⅎwnf 1781  Ⅎwnfc 2893   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-cleq 2732  df-nfc 2895  df-ne 2947

This theorem is referenced by:  cantnflem1  9758  ac6c4  10550  fproddiv  16009  fprodn0  16027  fproddivf  16035  mreiincl  17654  lss1d  20984  iunconn  23457  restmetu  24604  coeeq2  26301  sltval2  27719  fedgmullem2  33643  bnj1534  34829  bnj1542  34833  bnj1398  35010  bnj1445  35020  bnj1449  35024  bnj1312  35034  bnj1525  35045  cvmcov  35231  nfwlim  35786  finminlem  36284  finxpreclem2  37356  poimirlem25  37605  poimirlem26  37606  poimirlem28  37608  cdleme40m  40424  cdleme40n  40425  dihglblem5  41255  iunconnlem2  44906  eliuniin2  45022  disjf1  45090  disjrnmpt2  45095  disjinfi  45099  allbutfiinf  45335  fsumiunss  45496  idlimc  45547  0ellimcdiv  45570  stoweidlem31  45952  stoweidlem58  45979  fourierdlem31  46059  sge0iunmpt  46339