Theorem suceq 3038

Description: Equality of successors.

Assertion

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

Proof of Theorem suceq

Step	Hyp	Ref	Expression
1		sneq 2475	. . . 4 |- (A = B -> {A} = {B})
2	1	uneq2d 2236	. . 3 |- (A = B -> (A u. {A}) = (A u. {B}))
3		uneq1 2229	. . 3 |- (A = B -> (A u. {B}) = (B u. {B}))
4	2, 3	eqtrd 1550	. 2 |- (A = B -> (A u. {A}) = (B u. {B}))
5		df-suc 2981	. 2 |- suc A = (A u. {A})
6		df-suc 2981	. 2 |- suc B = (B u. {B})
7	4, 5, 6	3eqtr4g 1574	1 |- (A = B -> suc A = suc B)

Syntax hints:   -> wi 3   = wceq 992   u. cun 2097  {csn 2467  suc csuc 2977

This theorem is referenced by:  sucidg 3052  eqelsuc 3054  suc11 3073  ordunisuc 3186  onuninsuci 3194  limsuc 3203  tfindes 3215  tfinds2 3216  findes 3248  rdgsuc 4246  oasuc 4299  oa1suc 4300  oa0r 4309  oaass 4331  oneo 4348  nnacom 4373  nnmsucr 4380  oaabs 4392  nneob 4395  omsmolem 4396  limensuc 4654  nneneq 4659  unblem2 4687  unblem3 4688  suc11reg 4750  inf0 4751  inf3lem1 4758  dfom3 4776  infensuc 4784  rankid 4818  rankr1 4820  ranklim 4831  rankop 4839  rankelun 4853  rankelop 4855  rankxpu 4857  rankxplim 4858  cardsucnn 4971  sucxpdom 4996  nnacda 5090  om2uzsuci 6659  cardfz 6671  top2usne 11051  dif1card 11835

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-sn 2470  df-suc 2981

Copyright terms: Public domain