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

Theorem coeq2 5031
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 5029 . . 3  |-  ( A 
C_  B  ->  ( C  o.  A )  C_  ( C  o.  B
) )
2 coss2 5029 . . 3  |-  ( B 
C_  A  ->  ( C  o.  B )  C_  ( C  o.  A
) )
31, 2anim12i 550 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  o.  A )  C_  ( C  o.  B )  /\  ( C  o.  B
)  C_  ( C  o.  A ) ) )
4 eqss 3363 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3363 . 2  |-  ( ( C  o.  A )  =  ( C  o.  B )  <->  ( ( C  o.  A )  C_  ( C  o.  B
)  /\  ( C  o.  B )  C_  ( C  o.  A )
) )
63, 4, 53imtr4i 258 1  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    C_ wss 3320    o. ccom 4882
This theorem is referenced by:  coeq2i  5033  coeq2d  5035  coi2  5386  relcnvtr  5389  relcoi1  5398  f1eqcocnv  6028  ereq1  6912  seqf1olem2  11363  seqf1o  11364  isps  14634  pwsco2mhm  14770  gsumwmhm  14790  frmdgsum  14807  frmdup1  14809  frmdup2  14810  symgov  15100  frgpuplem  15404  frgpupf  15405  frgpupval  15406  gsumval3eu  15513  gsumval3  15514  kgencn2  17589  upxp  17655  uptx  17657  txcn  17658  xkococnlem  17691  xkococn  17692  cnmptk1  17713  cnmptkk  17715  xkofvcn  17716  imasdsf1olem  18403  pi1cof  19084  pi1coval  19085  elovolmr  19372  ovoliunlem3  19400  ismbf1  19518  hocsubdir  23288  hoddi  23493  lnopco0i  23507  opsqrlem1  23643  pjsdi2i  23660  pjin2i  23696  pjclem1  23698  cvmliftmo  24971  cvmliftlem14  24984  cvmliftiota  24988  cvmlift2lem13  25002  cvmlift2  25003  cvmliftphtlem  25004  cvmlift3lem2  25007  cvmlift3lem6  25011  cvmlift3lem7  25012  cvmlift3lem9  25014  cvmlift3  25015  relexp0  25129  relexpsucr  25130  relexpsucl  25132  relexpadd  25138  ftc1anclem8  26287  upixp  26431  psgnunilem1  27393  mendmulr  27473  trlcoat  31520  trljco  31537  tgrpov  31545  tendovalco  31562  erngmul  31603  erngmul-rN  31611  dvamulr  31809  dvavadd  31812  dvhmulr  31884  dihjatcclem4  32219
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-in 3327  df-ss 3334  df-br 4213  df-opab 4267  df-co 4887
  Copyright terms: Public domain W3C validator