Theorem coeq2 5150

Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)

Assertion

Ref	Expression
coeq2	|- ( A = B -> ( C o. A ) = ( C o. B ) )

Proof of Theorem coeq2

Step	Hyp	Ref	Expression
1		coss2 5148	. . 3 |- ( A C_ B -> ( C o. A ) C_ ( C o. B ) )
2		coss2 5148	. . 3 |- ( B C_ A -> ( C o. B ) C_ ( C o. A ) )
3	1, 2	anim12i 564	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( ( C o. A ) C_ ( C o. B ) /\ ( C o. B ) C_ ( C o. A ) ) )
4		eqss 3504	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3504	. 2 |- ( ( C o. A ) = ( C o. B ) <-> ( ( C o. A ) C_ ( C o. B ) /\ ( C o. B ) C_ ( C o. A ) ) )
6	3, 4, 5	3imtr4i 266	1 |- ( A = B -> ( C o. A ) = ( C o. B ) )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   C_ wss 3461   o. ccom 4992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3468  df-ss 3475  df-br 4440  df-opab 4498  df-co 4997

This theorem is referenced by:  coeq2i  5152  coeq2d  5154  coi2  5507  relcnvtr  5510  relcoi1  5519  f1eqcocnv  6179  ereq1  7310  seqf1olem2  12129  seqf1o  12130  relexpsucnnr  12942  isps  16031  pwsco2mhm  16201  gsumwmhm  16212  frmdgsum  16229  frmdup1  16231  frmdup2  16232  symgov  16614  pmtr3ncom  16699  psgnunilem1  16717  frgpuplem  16989  frgpupf  16990  frgpupval  16991  gsumval3eu  17106  gsumval3OLD  17107  gsumval3lem2  17109  kgencn2  20224  upxp  20290  uptx  20292  txcn  20293  xkococnlem  20326  xkococn  20327  cnmptk1  20348  cnmptkk  20350  xkofvcn  20351  imasdsf1olem  21042  pi1cof  21725  pi1coval  21726  elovolmr  22053  ovoliunlem3  22081  ismbf1  22199  motplusg  24130  hocsubdir  26902  hoddi  27107  lnopco0i  27121  opsqrlem1  27257  pjsdi2i  27274  pjin2i  27310  pjclem1  27312  eulerpartgbij  28575  cvmliftmo  28993  cvmliftlem14  29006  cvmliftiota  29010  cvmlift2lem13  29024  cvmlift2  29025  cvmliftphtlem  29026  cvmlift3lem2  29029  cvmlift3lem6  29033  cvmlift3lem7  29034  cvmlift3lem9  29036  cvmlift3  29037  msubco  29155  ftc1anclem8  30337  upixp  30460  mendmulr  31378  rngcinv  33043  rngcinvALTV  33055  ringcinv  33094  ringcinvALTV  33118  trlcoat  36846  trljco  36863  tgrpov  36871  tendovalco  36888  erngmul  36929  erngmul-rN  36937  dvamulr  37135  dvavadd  37138  dvhmulr  37210  dihjatcclem4  37545