Theorem suceq 5933

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 4326	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	uneq12d 3919	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ {𝐴}) = (𝐵 ∪ {𝐵}))
4		df-suc 5872	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
5		df-suc 5872	. 2 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
6	3, 4, 5	3eqtr4g 2830	1 ⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)

Syntax hints:   → wi 4   = wceq 1631   ∪ cun 3721  {csn 4316  suc csuc 5868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-sn 4317  df-suc 5872

This theorem is referenced by:  eqelsuc  5949  suc11  5974  ordunisuc  7179  onsucuni2  7181  onuninsuci  7187  limsuc  7196  tfindes  7209  tfinds2  7210  findes  7243  onnseq  7594  seqomlem0  7697  seqomlem1  7698  seqomlem4  7701  oasuc  7758  onasuc  7762  oa1suc  7765  oa0r  7772  o2p2e4  7775  oaass  7795  oneo  7815  omeulem1  7816  oeeulem  7835  oeeui  7836  nna0r  7843  nnacom  7851  nnaass  7856  nnmsucr  7859  omabs  7881  nnneo  7885  nneob  7886  omsmolem  7887  omopthlem1  7889  limensuc  8293  infensuc  8294  nneneq  8299  unblem2  8369  unblem3  8370  suc11reg  8680  inf0  8682  inf3lem1  8689  dfom3  8708  cantnflt  8733  cantnflem1  8750  cnfcom  8761  r1elwf  8823  rankidb  8827  rankonidlem  8855  ranklim  8871  rankopb  8879  rankelop  8901  rankxpu  8903  rankmapu  8905  rankxplim  8906  cardsucnn  9011  dif1card  9033  infxpenlem  9036  fseqenlem1  9047  dfac12lem1  9167  dfac12lem2  9168  dfac12r  9170  pwsdompw  9228  ackbij1lem14  9257  ackbij1lem18  9261  ackbij1  9262  ackbij2lem3  9265  cfsmolem  9294  cfsmo  9295  sornom  9301  isfin3ds  9353  isf32lem1  9377  isf32lem2  9378  isf32lem5  9381  isf32lem6  9382  isf32lem7  9383  isf32lem8  9384  isf32lem11  9387  fin1a2lem1  9424  ituniiun  9446  axdc2lem  9472  axdc3lem2  9475  axdc3lem3  9476  axdc3lem4  9477  axdc3  9478  axdc4lem  9479  axcclem  9481  axdclem2  9544  wunex2  9762  om2uzsuci  12955  axdc4uzlem  12990  bnj222  31291  bnj966  31352  bnj1112  31389  noresle  32183  nosupno  32186  nosupdm  32187  nosupfv  32189  nosupres  32190  nosupbnd1lem1  32191  nosupbnd1lem3  32193  nosupbnd1lem5  32195  nosupbnd2  32199  noetalem4  32203  noeta  32205  rankaltopb  32423  ranksng  32611  rankpwg  32613  rankeq1o  32615  ontgsucval  32768  onsucconn  32774  onsucsuccmp  32780  limsucncmp  32782  ordcmp  32783  finxpreclem4  33568  finxp00  33576  limsuc2  38137  aomclem4  38153  aomclem8  38157  onsetreclem1  42979