MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coeq2 Unicode version

Theorem coeq2 4842
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
StepHypRef Expression
1 coss2 4840 . . 3  |-  ( A 
C_  B  ->  ( C  o.  A )  C_  ( C  o.  B
) )
2 coss2 4840 . . 3  |-  ( B 
C_  A  ->  ( C  o.  B )  C_  ( C  o.  A
) )
31, 2anim12i 549 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  o.  A )  C_  ( C  o.  B )  /\  ( C  o.  B
)  C_  ( C  o.  A ) ) )
4 eqss 3194 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3194 . 2  |-  ( ( C  o.  A )  =  ( C  o.  B )  <->  ( ( C  o.  A )  C_  ( C  o.  B
)  /\  ( C  o.  B )  C_  ( C  o.  A )
) )
63, 4, 53imtr4i 257 1  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    C_ wss 3152    o. ccom 4693
This theorem is referenced by:  coeq2i  4844  coeq2d  4846  coi2  5189  relcnvtr  5192  relcoi1  5201  f1eqcocnv  5805  ereq1  6667  seqf1olem2  11086  seqf1o  11087  isps  14311  pwsco2mhm  14447  gsumwmhm  14467  frmdgsum  14484  frmdup1  14486  frmdup2  14487  symgov  14777  frgpuplem  15081  frgpupf  15082  frgpupval  15083  gsumval3eu  15190  gsumval3  15191  kgencn2  17252  upxp  17317  uptx  17319  txcn  17320  xkococnlem  17353  xkococn  17354  cnmptk1  17375  cnmptkk  17377  xkofvcn  17378  imasdsf1olem  17937  pi1cof  18557  pi1coval  18558  elovolmr  18835  ovoliunlem3  18863  ismbf1  18981  hocsubdir  22365  hoddi  22570  lnopco0i  22584  opsqrlem1  22720  pjsdi2i  22737  pjin2i  22773  pjclem1  22775  cvmliftmo  23815  cvmliftlem14  23828  cvmliftiota  23832  cvmlift2lem13  23846  cvmlift2  23847  cvmliftphtlem  23848  cvmlift3lem2  23851  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  cvmlift3  23859  relexp0  24025  relexpsucr  24026  relexpsucl  24028  relexpadd  24035  ov2gc  25123  mapmapmap  25148  injsurinj  25149  isprsr  25224  upixp  26403  psgnunilem1  27416  mendmulr  27496  trlcoat  30912  trljco  30929  tgrpov  30937  tendovalco  30954  erngmul  30995  erngmul-rN  31003  dvamulr  31201  dvavadd  31204  dvhmulr  31276  dihjatcclem4  31611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-co 4698
  Copyright terms: Public domain W3C validator