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

Theorem coeq1 5021
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 5019 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 5019 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 550 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3355 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3355 . 2  |-  ( ( A  o.  C )  =  ( B  o.  C )  <->  ( ( A  o.  C )  C_  ( B  o.  C
)  /\  ( B  o.  C )  C_  ( A  o.  C )
) )
63, 4, 53imtr4i 258 1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    C_ wss 3312    o. ccom 4873
This theorem is referenced by:  coeq1i  5023  coeq1d  5025  coi2  5377  relcnvtr  5380  funcoeqres  5697  ereq1  6903  domssex2  7258  wemapwe  7643  seqf1olem2  11351  seqf1o  11352  isps  14622  pwsco1mhm  14757  frmdup3  14799  symgov  15088  frgpup3  15398  gsumval3  15502  frgpcyg  16842  xkococnlem  17679  xkococn  17680  cnmpt1k  17702  cnmptkk  17703  xkofvcn  17704  qtopeu  17736  qtophmeo  17837  utop2nei  18268  cncombf  19538  evlseu  19925  evlsval2  19929  evl1val  19936  mpfpf1  19959  pf1mpf  19960  pf1ind  19963  dgrcolem2  20180  dgrco  20181  hocsubdir  23276  hoddi  23481  opsqrlem1  23631  relexpsucr  25118  relexp1  25119  relexpsucl  25120  diophrw  26754  eldioph2  26757  diophren  26811  frlmup4  27168  psgnunilem1  27331  mendmulr  27411  trljco  31376  tgrpov  31384  tendovalco  31401  erngmul  31442  erngmul-rN  31450  cdlemksv  31480  cdlemkuu  31531  cdlemk41  31556  cdleml5N  31616  cdleml9  31620  dvamulr  31648  dvavadd  31651  dvhmulr  31723  dvhvscacbv  31735  dvhvscaval  31736  dih1dimatlem0  31965  dihjatcclem4  32058
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-in 3319  df-ss 3326  df-br 4205  df-opab 4259  df-co 4878
  Copyright terms: Public domain W3C validator