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

Theorem coeq1 5160
Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
Assertion
Ref Expression
coeq1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )

Proof of Theorem coeq1
StepHypRef Expression
1 coss1 5158 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 5158 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 566 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3519 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3519 . 2  |-  ( ( A  o.  C )  =  ( B  o.  C )  <->  ( ( A  o.  C )  C_  ( B  o.  C
)  /\  ( B  o.  C )  C_  ( A  o.  C )
) )
63, 4, 53imtr4i 266 1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
Colors of variables: wff setvar class
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:  coeq1i  5162  coeq1d  5164  coi2  5524  relcnvtr  5527  funcoeqres  5846  ereq1  7318  domssex2  7677  wemapwe  8139  wemapweOLD  8140  seqf1olem2  12115  seqf1o  12116  isps  15689  pwsco1mhm  15820  frmdup3  15866  symgov  16220  pmtr3ncom  16306  psgnunilem1  16324  frgpup3  16602  gsumval3OLD  16711  gsumval3  16714  evlseu  17984  evlsval2  17988  evls1val  18156  evls1sca  18159  evl1val  18164  mpfpf1  18186  pf1mpf  18187  pf1ind  18190  frgpcyg  18407  frlmup4  18630  xkococnlem  19923  xkococn  19924  cnmpt1k  19946  cnmptkk  19947  xkofvcn  19948  qtopeu  19980  qtophmeo  20081  utop2nei  20516  cncombf  21828  dgrcolem2  22433  dgrco  22434  motplusg  23685  hocsubdir  26408  hoddi  26613  opsqrlem1  26763  relexpsucr  28556  relexp1  28557  relexpsucl  28558  diophrw  30324  eldioph2  30327  diophren  30379  mendmulr  30770  trljco  35554  tgrpov  35562  tendovalco  35579  erngmul  35620  erngmul-rN  35628  cdlemksv  35658  cdlemkuu  35709  cdlemk41  35734  cdleml5N  35794  cdleml9  35798  dvamulr  35826  dvavadd  35829  dvhmulr  35901  dvhvscacbv  35913  dvhvscaval  35914  dih1dimatlem0  36143  dihjatcclem4  36236
  Copyright terms: Public domain W3C validator