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 566	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( ( C o. A ) C_ ( C o. B ) /\ ( C o. B ) C_ ( C o. A ) ) )
4		eqss 3371	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3371	. 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 1369   C_ wss 3328   o. ccom 4844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-in 3335  df-ss 3342  df-br 4293  df-opab 4351  df-co 4849

This theorem is referenced by:  coeq2i  5000  coeq2d  5002  coi2  5354  relcnvtr  5357  relcoi1  5366  f1eqcocnv  5999  ereq1  7108  seqf1olem2  11846  seqf1o  11847  isps  15372  pwsco2mhm  15499  gsumwmhm  15523  frmdgsum  15540  frmdup1  15542  frmdup2  15543  symgov  15895  pmtr3ncom  15981  psgnunilem1  15999  frgpuplem  16269  frgpupf  16270  frgpupval  16271  gsumval3eu  16381  gsumval3OLD  16382  gsumval3lem2  16384  kgencn2  19130  upxp  19196  uptx  19198  txcn  19199  xkococnlem  19232  xkococn  19233  cnmptk1  19254  cnmptkk  19256  xkofvcn  19257  imasdsf1olem  19948  pi1cof  20631  pi1coval  20632  elovolmr  20959  ovoliunlem3  20987  ismbf1  21104  hocsubdir  25189  hoddi  25394  lnopco0i  25408  opsqrlem1  25544  pjsdi2i  25561  pjin2i  25597  pjclem1  25599  eulerpartgbij  26755  cvmliftmo  27173  cvmliftlem14  27186  cvmliftiota  27190  cvmlift2lem13  27204  cvmlift2  27205  cvmliftphtlem  27206  cvmlift3lem2  27209  cvmlift3lem6  27213  cvmlift3lem7  27214  cvmlift3lem9  27216  cvmlift3  27217  relexp0  27331  relexpsucr  27332  relexpsucl  27334  relexpadd  27340  ftc1anclem8  28474  upixp  28623  mendmulr  29545  trlcoat  34367  trljco  34384  tgrpov  34392  tendovalco  34409  erngmul  34450  erngmul-rN  34458  dvamulr  34656  dvavadd  34659  dvhmulr  34731  dihjatcclem4  35066