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

Theorem coeq1 5033
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 5031 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 5031 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 551 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3365 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3365 . 2  |-  ( ( A  o.  C )  =  ( B  o.  C )  <->  ( ( A  o.  C )  C_  ( B  o.  C
)  /\  ( B  o.  C )  C_  ( A  o.  C )
) )
63, 4, 53imtr4i 259 1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    C_ wss 3322    o. ccom 4885
This theorem is referenced by:  coeq1i  5035  coeq1d  5037  coi2  5389  relcnvtr  5392  funcoeqres  5709  ereq1  6915  domssex2  7270  wemapwe  7657  seqf1olem2  11368  seqf1o  11369  isps  14639  pwsco1mhm  14774  frmdup3  14816  symgov  15105  frgpup3  15415  gsumval3  15519  frgpcyg  16859  xkococnlem  17696  xkococn  17697  cnmpt1k  17719  cnmptkk  17720  xkofvcn  17721  qtopeu  17753  qtophmeo  17854  utop2nei  18285  cncombf  19553  evlseu  19942  evlsval2  19946  evl1val  19953  mpfpf1  19976  pf1mpf  19977  pf1ind  19980  dgrcolem2  20197  dgrco  20198  hocsubdir  23293  hoddi  23498  opsqrlem1  23648  relexpsucr  25135  relexp1  25136  relexpsucl  25137  diophrw  26830  eldioph2  26833  diophren  26887  frlmup4  27243  psgnunilem1  27406  mendmulr  27486  trljco  31610  tgrpov  31618  tendovalco  31635  erngmul  31676  erngmul-rN  31684  cdlemksv  31714  cdlemkuu  31765  cdlemk41  31790  cdleml5N  31850  cdleml9  31854  dvamulr  31882  dvavadd  31885  dvhmulr  31957  dvhvscacbv  31969  dvhvscaval  31970  dih1dimatlem0  32199  dihjatcclem4  32292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-in 3329  df-ss 3336  df-br 4216  df-opab 4270  df-co 4890
  Copyright terms: Public domain W3C validator