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

Theorem coeq1 4841
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 4839 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 4839 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 549 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3194 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3194 . 2  |-  ( ( A  o.  C )  =  ( B  o.  C )  <->  ( ( A  o.  C )  C_  ( B  o.  C
)  /\  ( B  o.  C )  C_  ( A  o.  C )
) )
63, 4, 53imtr4i 257 1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    C_ wss 3152    o. ccom 4693
This theorem is referenced by:  coeq1i  4843  coeq1d  4845  coi2  5189  relcnvtr  5192  funcoeqres  5504  ereq1  6667  domssex2  7021  wemapwe  7400  seqf1olem2  11086  seqf1o  11087  isps  14311  pwsco1mhm  14446  frmdup3  14488  symgov  14777  frgpup3  15087  gsumval3  15191  frgpcyg  16527  xkococnlem  17353  xkococn  17354  cnmpt1k  17376  cnmptkk  17377  xkofvcn  17378  qtopeu  17407  qtophmeo  17508  cncombf  19013  evlseu  19400  evlsval2  19404  evl1val  19411  mpfpf1  19434  pf1mpf  19435  pf1ind  19438  dgrcolem2  19655  dgrco  19656  hocsubdir  22365  hoddi  22570  opsqrlem1  22720  relexpsucr  24026  relexp1  24027  relexpsucl  24028  injrec2  25119  ov2gc  25123  cur1val  25198  isprsr  25224  diophrw  26838  eldioph2  26841  diophren  26896  frlmup4  27253  psgnunilem1  27416  mendmulr  27496  trljco  30929  tgrpov  30937  tendovalco  30954  erngmul  30995  erngmul-rN  31003  cdlemksv  31033  cdlemkuu  31084  cdlemk41  31109  cdleml5N  31169  cdleml9  31173  dvamulr  31201  dvavadd  31204  dvhmulr  31276  dvhvscacbv  31288  dvhvscaval  31289  dih1dimatlem0  31518  dihjatcclem4  31611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-co 4698
  Copyright terms: Public domain W3C validator