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

Theorem coeq1 4970
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 4968 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 4968 . . 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 3306 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3306 . 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 1649    C_ wss 3263    o. ccom 4822
This theorem is referenced by:  coeq1i  4972  coeq1d  4974  coi2  5326  relcnvtr  5329  funcoeqres  5646  ereq1  6848  domssex2  7203  wemapwe  7587  seqf1olem2  11290  seqf1o  11291  isps  14561  pwsco1mhm  14696  frmdup3  14738  symgov  15027  frgpup3  15337  gsumval3  15441  frgpcyg  16777  xkococnlem  17612  xkococn  17613  cnmpt1k  17635  cnmptkk  17636  xkofvcn  17637  qtopeu  17669  qtophmeo  17770  utop2nei  18201  cncombf  19417  evlseu  19804  evlsval2  19808  evl1val  19815  mpfpf1  19838  pf1mpf  19839  pf1ind  19842  dgrcolem2  20059  dgrco  20060  hocsubdir  23136  hoddi  23341  opsqrlem1  23491  relexpsucr  24909  relexp1  24910  relexpsucl  24911  diophrw  26508  eldioph2  26511  diophren  26565  frlmup4  26922  psgnunilem1  27085  mendmulr  27165  trljco  30854  tgrpov  30862  tendovalco  30879  erngmul  30920  erngmul-rN  30928  cdlemksv  30958  cdlemkuu  31009  cdlemk41  31034  cdleml5N  31094  cdleml9  31098  dvamulr  31126  dvavadd  31129  dvhmulr  31201  dvhvscacbv  31213  dvhvscaval  31214  dih1dimatlem0  31443  dihjatcclem4  31536
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-in 3270  df-ss 3277  df-br 4154  df-opab 4208  df-co 4827
  Copyright terms: Public domain W3C validator