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

Theorem coeq1 5010
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 5008 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 5008 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 574 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3458 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3458 . 2  |-  ( ( A  o.  C )  =  ( B  o.  C )  <->  ( ( A  o.  C )  C_  ( B  o.  C
)  /\  ( B  o.  C )  C_  ( A  o.  C )
) )
63, 4, 53imtr4i 274 1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1454    C_ wss 3415    o. ccom 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-in 3422  df-ss 3429  df-br 4416  df-opab 4475  df-co 4861
This theorem is referenced by:  coeq1i  5012  coeq1d  5014  coi2  5370  relcnvtr  5373  funcoeqres  5866  ereq1  7395  domssex2  7757  wemapwe  8227  seqf1olem2  12284  seqf1o  12285  relexpsucnnl  13143  isps  16496  pwsco1mhm  16665  frmdup3  16699  symgov  17079  pmtr3ncom  17164  psgnunilem1  17182  frgpup3  17476  gsumval3  17589  evlseu  18787  evlsval2  18791  evls1val  18957  evls1sca  18960  evl1val  18965  mpfpf1  18987  pf1mpf  18988  pf1ind  18991  frgpcyg  19192  frlmup4  19407  xkococnlem  20722  xkococn  20723  cnmpt1k  20745  cnmptkk  20746  xkofvcn  20747  qtopeu  20779  qtophmeo  20880  utop2nei  21313  cncombf  22662  dgrcolem2  23276  dgrco  23277  motplusg  24635  hocsubdir  27486  hoddi  27691  opsqrlem1  27841  smatfval  28669  msubco  30217  trljco  34351  tgrpov  34359  tendovalco  34376  erngmul  34417  erngmul-rN  34425  cdlemksv  34455  cdlemkuu  34506  cdlemk41  34531  cdleml5N  34591  cdleml9  34595  dvamulr  34623  dvavadd  34626  dvhmulr  34698  dvhvscacbv  34710  dvhvscaval  34711  dih1dimatlem0  34940  dihjatcclem4  35033  diophrw  35645  eldioph2  35648  diophren  35700  mendmulr  36098  rngcinv  40255  rngcinvALTV  40267  ringcinv  40306  ringcinvALTV  40330
  Copyright terms: Public domain W3C validator