Theorem coeq2 5280

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 5278	. . 3 |- ( A C_ B -> ( C o. A ) C_ ( C o. B ) )
2		coss2 5278	. . 3 |- ( B C_ A -> ( C o. B ) C_ ( C o. A ) )
3	1, 2	anim12i 590	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( ( C o. A ) C_ ( C o. B ) /\ ( C o. B ) C_ ( C o. A ) ) )
4		eqss 3618	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3618	. 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 281	1 |- ( A = B -> ( C o. A ) = ( C o. B ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   C_ wss 3574   o. ccom 5118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-co 5123

This theorem is referenced by:  coeq2i  5282  coeq2d  5284  coi2  5652  relcnvtr  5655  f1eqcocnv  6556  ereq1  7749  seqf1olem2  12841  seqf1o  12842  relexpsucnnr  13765  isps  17202  pwsco2mhm  17371  gsumwmhm  17382  frmdgsum  17399  frmdup1  17401  frmdup2  17402  symgov  17810  pmtr3ncom  17895  psgnunilem1  17913  frgpuplem  18185  frgpupf  18186  frgpupval  18187  gsumval3eu  18305  gsumval3lem2  18307  kgencn2  21360  upxp  21426  uptx  21428  txcn  21429  xkococnlem  21462  xkococn  21463  cnmptk1  21484  cnmptkk  21486  xkofvcn  21487  imasdsf1olem  22178  pi1cof  22859  pi1coval  22860  elovolmr  23244  ovoliunlem3  23272  ismbf1  23393  motplusg  25437  hocsubdir  28644  hoddi  28849  lnopco0i  28863  opsqrlem1  28999  pjsdi2i  29016  pjin2i  29052  pjclem1  29054  symgfcoeu  29845  eulerpartgbij  30434  cvmliftmo  31266  cvmliftlem14  31279  cvmliftiota  31283  cvmlift2lem13  31297  cvmlift2  31298  cvmliftphtlem  31299  cvmlift3lem2  31302  cvmlift3lem6  31306  cvmlift3lem7  31307  cvmlift3lem9  31309  cvmlift3  31310  msubco  31428  ftc1anclem8  33492  upixp  33524  coideq  34009  trlcoat  36011  trljco  36028  tgrpov  36036  tendovalco  36053  erngmul  36094  erngmul-rN  36102  dvamulr  36300  dvavadd  36303  dvhmulr  36375  dihjatcclem4  36710  mendmulr  37758  hoiprodcl2  40769  ovnlecvr  40772  ovncvrrp  40778  ovnsubaddlem2  40785  ovncvr2  40825  opnvonmbllem1  40846  opnvonmbl  40848  ovolval4lem2  40864  ovolval5lem2  40867  ovolval5lem3  40868  ovolval5  40869  ovnovollem2  40871  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056