Theorem suceq 2288

Description: Equality of successors.

Assertion

Ref	Expression
suceq	⊢ (A = B → suc A = suc B)

Proof of Theorem suceq

Step	Hyp	Ref	Expression
1		sneq 1816	. . . 4 ⊢ (A = B → {A} = {B})
2	1	uneq2d 1611	. . 3 ⊢ (A = B → (A ∪ {A}) = (A ∪ {B}))
3		uneq1 1605	. . 3 ⊢ (A = B → (A ∪ {B}) = (B ∪ {B}))
4	2, 3	eqtrd 1128	. 2 ⊢ (A = B → (A ∪ {A}) = (B ∪ {B}))
5		df-suc 2205	. 2 ⊢ suc A = (A ∪ {A})
6		df-suc 2205	. 2 ⊢ suc B = (B ∪ {B})
7	4, 5, 6	3eqtr4g 1147	1 ⊢ (A = B → suc A = suc B)

Syntax hints:   → wi 2   = wceq 1091   ∪ cun 1485  {csn 1808  suc csuc 2201

This theorem is referenced by:  sucidg 2305  eqelsuc 2307  ordunisuc 2339  suc11 2341  onuninsuc 2356  limsuc 2361  findes 2400  tfindes 2404  tfinds2 2405  rdgsuct 2983  oasuc 3131  oa1suc 3132  oa0r 3141  oaass 3163  nnacom 3175  nnmsucr 3182  omsmolem 3195  limensuc 3402  nneneq 3408  unblem2 3432  unblem3 3433  suc11reg 3456  inf0 3457  inf3lem1 3464  dfom3 3477  infensuc 3484  rankid 3516  rankr1 3518  sucxpdom 3652  om2uzsuc 4652

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-suc 2205

metamath.org