Theorem suceq 3029

Description: Equality of successors.

Assertion

Ref	Expression
suceq	|- (A = B -> suc A = suc B)

Proof of Theorem suceq

Step	Hyp	Ref	Expression
1		sneq 2413	. . . 4 |- (A = B -> {A} = {B})
2	1	uneq2d 2180	. . 3 |- (A = B -> (A u. {A}) = (A u. {B}))
3		uneq1 2173	. . 3 |- (A = B -> (A u. {B}) = (B u. {B}))
4	2, 3	eqtrd 1504	. 2 |- (A = B -> (A u. {A}) = (B u. {B}))
5		df-suc 2949	. 2 |- suc A = (A u. {A})
6		df-suc 2949	. 2 |- suc B = (B u. {B})
7	4, 5, 6	3eqtr4g 1528	1 |- (A = B -> suc A = suc B)

Syntax hints:   -> wi 3   = wceq 954   u. cun 2041  {csn 2405  suc csuc 2945

This theorem is referenced by:  sucidg 3047  eqelsuc 3049  ordunisuc 3084  suc11 3088  onuninsuc 3103  limsuc 3115  findes 3155  tfindes 3159  tfinds2 3160  rdgsuct 3936  oasuc 4153  oa1suc 4154  oa0r 4163  oaass 4185  oneo 4202  nnacom 4223  nnmsucr 4230  oaabs 4242  nneob 4245  omsmolem 4246  limensuc 4493  nneneq 4498  unblem2 4524  unblem3 4525  suc11reg 4585  inf0 4586  inf3lem1 4593  dfom3 4610  infensuc 4618  rankid 4652  rankr1 4654  ranklim 4665  rankop 4673  rankelun 4687  rankelop 4689  rankxpu 4691  rankxplim 4692  sucxpdom 4826  om2uzsuc 6241

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-suc 2949

Copyright terms: Public domain