Theorem coeq2 5160

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 5158	. . 3 |- ( A C_ B -> ( C o. A ) C_ ( C o. B ) )
2		coss2 5158	. . 3 |- ( B C_ A -> ( C o. B ) C_ ( C o. A ) )
3	1, 2	anim12i 566	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( ( C o. A ) C_ ( C o. B ) /\ ( C o. B ) C_ ( C o. A ) ) )
4		eqss 3519	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3519	. 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 369   = wceq 1379   C_ wss 3476   o. ccom 5003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490  df-br 4448  df-opab 4506  df-co 5008

This theorem is referenced by:  coeq2i  5162  coeq2d  5164  coi2  5523  relcnvtr  5526  relcoi1  5535  f1eqcocnv  6191  ereq1  7318  seqf1olem2  12114  seqf1o  12115  isps  15688  pwsco2mhm  15818  gsumwmhm  15842  frmdgsum  15859  frmdup1  15861  frmdup2  15862  symgov  16217  pmtr3ncom  16303  psgnunilem1  16321  frgpuplem  16593  frgpupf  16594  frgpupval  16595  gsumval3eu  16707  gsumval3OLD  16708  gsumval3lem2  16710  kgencn2  19809  upxp  19875  uptx  19877  txcn  19878  xkococnlem  19911  xkococn  19912  cnmptk1  19933  cnmptkk  19935  xkofvcn  19936  imasdsf1olem  20627  pi1cof  21310  pi1coval  21311  elovolmr  21638  ovoliunlem3  21666  ismbf1  21784  motplusg  23673  hocsubdir  26396  hoddi  26601  lnopco0i  26615  opsqrlem1  26751  pjsdi2i  26768  pjin2i  26804  pjclem1  26806  eulerpartgbij  27967  cvmliftmo  28385  cvmliftlem14  28398  cvmliftiota  28402  cvmlift2lem13  28416  cvmlift2  28417  cvmliftphtlem  28418  cvmlift3lem2  28421  cvmlift3lem6  28425  cvmlift3lem7  28426  cvmlift3lem9  28428  cvmlift3  28429  relexp0  28543  relexpsucr  28544  relexpsucl  28546  relexpadd  28552  ftc1anclem8  29690  upixp  29839  mendmulr  30758  trlcoat  35528  trljco  35545  tgrpov  35553  tendovalco  35570  erngmul  35611  erngmul-rN  35619  dvamulr  35817  dvavadd  35820  dvhmulr  35892  dihjatcclem4  36227