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

Theorem coeq1 5149
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 5147 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 5147 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 564 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3504 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3504 . 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 367    = wceq 1398    C_ wss 3461    o. ccom 4992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3468  df-ss 3475  df-br 4440  df-opab 4498  df-co 4997
This theorem is referenced by:  coeq1i  5151  coeq1d  5153  coi2  5507  relcnvtr  5510  funcoeqres  5828  ereq1  7310  domssex2  7670  wemapwe  8130  wemapweOLD  8131  seqf1olem2  12129  seqf1o  12130  relexpsucnnl  12947  isps  16031  pwsco1mhm  16200  frmdup3  16234  symgov  16614  pmtr3ncom  16699  psgnunilem1  16717  frgpup3  16995  gsumval3OLD  17107  gsumval3  17110  evlseu  18380  evlsval2  18384  evls1val  18552  evls1sca  18555  evl1val  18560  mpfpf1  18582  pf1mpf  18583  pf1ind  18586  frgpcyg  18785  frlmup4  19003  xkococnlem  20326  xkococn  20327  cnmpt1k  20349  cnmptkk  20350  xkofvcn  20351  qtopeu  20383  qtophmeo  20484  utop2nei  20919  cncombf  22231  dgrcolem2  22837  dgrco  22838  motplusg  24130  hocsubdir  26902  hoddi  27107  opsqrlem1  27257  msubco  29155  diophrw  30931  eldioph2  30934  diophren  30986  mendmulr  31378  rngcinv  33043  rngcinvALTV  33055  ringcinv  33094  ringcinvALTV  33118  trljco  36863  tgrpov  36871  tendovalco  36888  erngmul  36929  erngmul-rN  36937  cdlemksv  36967  cdlemkuu  37018  cdlemk41  37043  cdleml5N  37103  cdleml9  37107  dvamulr  37135  dvavadd  37138  dvhmulr  37210  dvhvscacbv  37222  dvhvscaval  37223  dih1dimatlem0  37452  dihjatcclem4  37545
  Copyright terms: Public domain W3C validator