Theorem suceq 3034

Description: Equality of successors.

Assertion

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

Proof of Theorem suceq

Step	Hyp	Ref	Expression
1		sneq 2417	. . . 4 |- (A = B -> {A} = {B})
2	1	uneq2d 2184	. . 3 |- (A = B -> (A u. {A}) = (A u. {B}))
3		uneq1 2177	. . 3 |- (A = B -> (A u. {B}) = (B u. {B}))
4	2, 3	eqtrd 1507	. 2 |- (A = B -> (A u. {A}) = (B u. {B}))
5		df-suc 2954	. 2 |- suc A = (A u. {A})
6		df-suc 2954	. 2 |- suc B = (B u. {B})
7	4, 5, 6	3eqtr4g 1531	1 |- (A = B -> suc A = suc B)

Syntax hints:   -> wi 3   = wceq 956   u. cun 2045  {csn 2409  suc csuc 2950

This theorem is referenced by:  sucidg 3052  eqelsuc 3054  ordunisuc 3089  suc11 3093  onuninsuc 3108  limsuc 3120  findes 3160  tfindes 3164  tfinds2 3165  rdgsuct 3945  oasuc 4163  oa1suc 4164  oa0r 4173  oaass 4195  oneo 4212  nnacom 4233  nnmsucr 4240  oaabs 4252  nneob 4255  omsmolem 4256  limensuc 4507  nneneq 4512  unblem2 4541  unblem3 4542  suc11reg 4605  inf0 4606  inf3lem1 4613  dfom3 4630  infensuc 4638  rankid 4672  rankr1 4674  ranklim 4685  rankop 4693  rankelun 4707  rankelop 4709  rankxpu 4711  rankxplim 4712  sucxpdom 4846  om2uzsuc 6296  top2usne 10549

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-suc 2954

Copyright terms: Public domain