Theorem coeq2 4998

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 4996	. . 3 |- ( A C_ B -> ( C o. A ) C_ ( C o. B ) )
2		coss2 4996	. . 3 |- ( B C_ A -> ( C o. B ) C_ ( C o. A ) )
3	1, 2	anim12i 576	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( ( C o. A ) C_ ( C o. B ) /\ ( C o. B ) C_ ( C o. A ) ) )
4		eqss 3433	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3433	. 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 274	1 |- ( A = B -> ( C o. A ) = ( C o. B ) )

Syntax hints:   -> wi 4   /\ wa 376   = wceq 1452   C_ wss 3390   o. ccom 4843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-in 3397  df-ss 3404  df-br 4396  df-opab 4455  df-co 4848

This theorem is referenced by:  coeq2i  5000  coeq2d  5002  coi2  5359  relcnvtr  5362  relcoi1OLD  5372  f1eqcocnv  6217  ereq1  7388  seqf1olem2  12291  seqf1o  12292  relexpsucnnr  13165  isps  16526  pwsco2mhm  16696  gsumwmhm  16707  frmdgsum  16724  frmdup1  16726  frmdup2  16727  symgov  17109  pmtr3ncom  17194  psgnunilem1  17212  frgpuplem  17500  frgpupf  17501  frgpupval  17502  gsumval3eu  17616  gsumval3lem2  17618  kgencn2  20649  upxp  20715  uptx  20717  txcn  20718  xkococnlem  20751  xkococn  20752  cnmptk1  20773  cnmptkk  20775  xkofvcn  20776  imasdsf1olem  21466  pi1cof  22168  pi1coval  22169  elovolmr  22507  ovoliunlem3  22535  ismbf1  22661  motplusg  24666  hocsubdir  27519  hoddi  27724  lnopco0i  27738  opsqrlem1  27874  pjsdi2i  27891  pjin2i  27927  pjclem1  27929  symgfcoeu  28682  eulerpartgbij  29278  cvmliftmo  30079  cvmliftlem14  30092  cvmliftiota  30096  cvmlift2lem13  30110  cvmlift2  30111  cvmliftphtlem  30112  cvmlift3lem2  30115  cvmlift3lem6  30119  cvmlift3lem7  30120  cvmlift3lem9  30122  cvmlift3  30123  msubco  30241  ftc1anclem8  32088  upixp  32120  trlcoat  34361  trljco  34378  tgrpov  34386  tendovalco  34403  erngmul  34444  erngmul-rN  34452  dvamulr  34650  dvavadd  34653  dvhmulr  34725  dihjatcclem4  35060  mendmulr  36125  hoiprodcl2  38495  ovnlecvr  38498  ovncvrrp  38504  ovnsubaddlem2  38511  ovncvr2  38551  opnvonmbllem1  38572  opnvonmbl  38574  ovolval4lem2  38590  ovolval5lem2  38593  ovolval5lem3  38594  ovolval5  38595  ovnovollem2  38597  rngcinv  40491  rngcinvALTV  40503  ringcinv  40542  ringcinvALTV  40566