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

Theorem coeq1 4989
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 4987 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 4987 . . 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 3323 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3323 . 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 3280    o. ccom 4841
This theorem is referenced by:  coeq1i  4991  coeq1d  4993  coi2  5345  relcnvtr  5348  funcoeqres  5665  ereq1  6871  domssex2  7226  wemapwe  7610  seqf1olem2  11318  seqf1o  11319  isps  14589  pwsco1mhm  14724  frmdup3  14766  symgov  15055  frgpup3  15365  gsumval3  15469  frgpcyg  16809  xkococnlem  17644  xkococn  17645  cnmpt1k  17667  cnmptkk  17668  xkofvcn  17669  qtopeu  17701  qtophmeo  17802  utop2nei  18233  cncombf  19503  evlseu  19890  evlsval2  19894  evl1val  19901  mpfpf1  19924  pf1mpf  19925  pf1ind  19928  dgrcolem2  20145  dgrco  20146  hocsubdir  23241  hoddi  23446  opsqrlem1  23596  relexpsucr  25083  relexp1  25084  relexpsucl  25085  diophrw  26707  eldioph2  26710  diophren  26764  frlmup4  27121  psgnunilem1  27284  mendmulr  27364  trljco  31222  tgrpov  31230  tendovalco  31247  erngmul  31288  erngmul-rN  31296  cdlemksv  31326  cdlemkuu  31377  cdlemk41  31402  cdleml5N  31462  cdleml9  31466  dvamulr  31494  dvavadd  31497  dvhmulr  31569  dvhvscacbv  31581  dvhvscaval  31582  dih1dimatlem0  31811  dihjatcclem4  31904
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-in 3287  df-ss 3294  df-br 4173  df-opab 4227  df-co 4846
  Copyright terms: Public domain W3C validator