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

Theorem coeq1 4996
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 4994 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 4994 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 566 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3370 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3370 . 2  |-  ( ( A  o.  C )  =  ( B  o.  C )  <->  ( ( A  o.  C )  C_  ( B  o.  C
)  /\  ( B  o.  C )  C_  ( A  o.  C )
) )
63, 4, 53imtr4i 266 1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    C_ wss 3327    o. ccom 4843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-in 3334  df-ss 3341  df-br 4292  df-opab 4350  df-co 4848
This theorem is referenced by:  coeq1i  4998  coeq1d  5000  coi2  5353  relcnvtr  5356  funcoeqres  5670  ereq1  7107  domssex2  7470  wemapwe  7927  wemapweOLD  7928  seqf1olem2  11845  seqf1o  11846  isps  15371  pwsco1mhm  15497  frmdup3  15543  symgov  15894  pmtr3ncom  15980  psgnunilem1  15998  frgpup3  16274  gsumval3OLD  16381  gsumval3  16384  evlseu  17601  evlsval2  17605  evls1val  17754  evls1sca  17757  evl1val  17762  mpfpf1  17784  pf1mpf  17785  pf1ind  17788  frgpcyg  18005  frlmup4  18228  xkococnlem  19231  xkococn  19232  cnmpt1k  19254  cnmptkk  19255  xkofvcn  19256  qtopeu  19288  qtophmeo  19389  utop2nei  19824  cncombf  21135  dgrcolem2  21740  dgrco  21741  hocsubdir  25188  hoddi  25393  opsqrlem1  25543  relexpsucr  27331  relexp1  27332  relexpsucl  27333  diophrw  29095  eldioph2  29098  diophren  29150  mendmulr  29543  trljco  34382  tgrpov  34390  tendovalco  34407  erngmul  34448  erngmul-rN  34456  cdlemksv  34486  cdlemkuu  34537  cdlemk41  34562  cdleml5N  34622  cdleml9  34626  dvamulr  34654  dvavadd  34657  dvhmulr  34729  dvhvscacbv  34741  dvhvscaval  34742  dih1dimatlem0  34971  dihjatcclem4  35064
  Copyright terms: Public domain W3C validator