Theorem suceq 6256

Description: Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
suceq	⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Proof of Theorem suceq

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		sneq 4537	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 4064	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 6197	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 6197	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1543   ∪ cun 3851  {csn 4527  suc csuc 6193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-sn 4528  df-suc 6197

This theorem is referenced by:  eqelsuc  6272  suc11  6294  ordunisuc  7589  onsucuni2  7591  onuninsuci  7597  limsuc  7606  tfindes  7619  tfinds2  7620  peano5  7649  findes  7658  onnseq  8059  seqomlem0  8163  seqomlem1  8164  seqomlem4  8167  oasuc  8229  onasuc  8233  oa1suc  8236  oa0r  8243  o2p2e4  8246  o2p2e4OLD  8247  oaass  8267  oneo  8287  omeulem1  8288  oeeulem  8307  oeeui  8308  nna0r  8315  nnacom  8323  nnaass  8328  nnmsucr  8331  omabs  8354  nnneo  8358  nneob  8359  omsmolem  8360  omopthlem1  8362  limensuc  8801  infensuc  8802  nneneq  8807  unblem2  8902  unblem3  8903  suc11reg  9212  inf0  9214  inf3lem1  9221  dfom3  9240  cantnflt  9265  cantnflem1  9282  cnfcom  9293  r1elwf  9377  rankidb  9381  rankonidlem  9409  ranklim  9425  rankopb  9433  rankelop  9455  rankxpu  9457  rankmapu  9459  rankxplim  9460  cardsucnn  9566  dif1card  9589  infxpenlem  9592  fseqenlem1  9603  dfac12lem1  9722  dfac12lem2  9723  dfac12r  9725  pwsdompw  9783  ackbij1lem14  9812  ackbij1lem18  9816  ackbij1  9817  ackbij2lem3  9820  cfsmolem  9849  cfsmo  9850  sornom  9856  isfin3ds  9908  isf32lem1  9932  isf32lem2  9933  isf32lem5  9936  isf32lem6  9937  isf32lem7  9938  isf32lem8  9939  isf32lem11  9942  fin1a2lem1  9979  ituniiun  10001  axdc2lem  10027  axdc3lem2  10030  axdc3lem3  10031  axdc3lem4  10032  axdc3  10033  axdc4lem  10034  axcclem  10036  axdclem2  10099  wunex2  10317  om2uzsuci  13486  axdc4uzlem  13521  bnj222  32530  bnj966  32591  bnj1112  32630  gonar  33024  goalr  33026  satffun  33038  noresle  33586  nosupcbv  33591  nosupno  33592  nosupdm  33593  nosupfv  33595  nosupres  33596  nosupbnd1lem1  33597  nosupbnd1lem3  33599  nosupbnd1lem5  33601  nosupbnd2  33605  noinfcbv  33606  noinfno  33607  noinfdm  33608  noinffv  33610  noinfres  33611  noinfbnd1lem3  33614  noinfbnd1lem5  33616  bday1s  33711  rankaltopb  33967  ranksng  34155  rankpwg  34157  rankeq1o  34159  ontgsucval  34307  onsucconn  34313  onsucsuccmp  34319  limsucncmp  34321  ordcmp  34322  finxpreclem4  35251  finxp00  35259  limsuc2  40510  aomclem4  40526  aomclem8  40530  suceqd  41441  onsetreclem1  46024