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

Theorem coeq1 4954
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 4952 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 4952 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 568 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3422 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3422 . 2  |-  ( ( A  o.  C )  =  ( B  o.  C )  <->  ( ( A  o.  C )  C_  ( B  o.  C
)  /\  ( B  o.  C )  C_  ( A  o.  C )
) )
63, 4, 53imtr4i 269 1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    C_ wss 3379    o. ccom 4800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-in 3386  df-ss 3393  df-br 4367  df-opab 4426  df-co 4805
This theorem is referenced by:  coeq1i  4956  coeq1d  4958  coi2  5314  relcnvtr  5317  funcoeqres  5804  ereq1  7325  domssex2  7685  wemapwe  8154  seqf1olem2  12203  seqf1o  12204  relexpsucnnl  13039  isps  16391  pwsco1mhm  16560  frmdup3  16594  symgov  16974  pmtr3ncom  17059  psgnunilem1  17077  frgpup3  17371  gsumval3  17484  evlseu  18682  evlsval2  18686  evls1val  18852  evls1sca  18855  evl1val  18860  mpfpf1  18882  pf1mpf  18883  pf1ind  18886  frgpcyg  19086  frlmup4  19301  xkococnlem  20616  xkococn  20617  cnmpt1k  20639  cnmptkk  20640  xkofvcn  20641  qtopeu  20673  qtophmeo  20774  utop2nei  21207  cncombf  22556  dgrcolem2  23170  dgrco  23171  motplusg  24529  hocsubdir  27380  hoddi  27585  opsqrlem1  27735  smatfval  28573  msubco  30121  trljco  34219  tgrpov  34227  tendovalco  34244  erngmul  34285  erngmul-rN  34293  cdlemksv  34323  cdlemkuu  34374  cdlemk41  34399  cdleml5N  34459  cdleml9  34463  dvamulr  34491  dvavadd  34494  dvhmulr  34566  dvhvscacbv  34578  dvhvscaval  34579  dih1dimatlem0  34808  dihjatcclem4  34901  diophrw  35513  eldioph2  35516  diophren  35568  mendmulr  35967  rngcinv  39574  rngcinvALTV  39586  ringcinv  39625  ringcinvALTV  39649
  Copyright terms: Public domain W3C validator