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

Theorem coeq1 4857
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 4855 . . 3  |-  ( A 
C_  B  ->  ( A  o.  C )  C_  ( B  o.  C
) )
2 coss1 4855 . . 3  |-  ( B 
C_  A  ->  ( B  o.  C )  C_  ( A  o.  C
) )
31, 2anim12i 549 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( A  o.  C )  C_  ( B  o.  C )  /\  ( B  o.  C
)  C_  ( A  o.  C ) ) )
4 eqss 3207 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3207 . 2  |-  ( ( A  o.  C )  =  ( B  o.  C )  <->  ( ( A  o.  C )  C_  ( B  o.  C
)  /\  ( B  o.  C )  C_  ( A  o.  C )
) )
63, 4, 53imtr4i 257 1  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    C_ wss 3165    o. ccom 4709
This theorem is referenced by:  coeq1i  4859  coeq1d  4861  coi2  5205  relcnvtr  5208  funcoeqres  5520  ereq1  6683  domssex2  7037  wemapwe  7416  seqf1olem2  11102  seqf1o  11103  isps  14327  pwsco1mhm  14462  frmdup3  14504  symgov  14793  frgpup3  15103  gsumval3  15207  frgpcyg  16543  xkococnlem  17369  xkococn  17370  cnmpt1k  17392  cnmptkk  17393  xkofvcn  17394  qtopeu  17423  qtophmeo  17524  cncombf  19029  evlseu  19416  evlsval2  19420  evl1val  19427  mpfpf1  19450  pf1mpf  19451  pf1ind  19454  dgrcolem2  19671  dgrco  19672  hocsubdir  22381  hoddi  22586  opsqrlem1  22736  relexpsucr  24041  relexp1  24042  relexpsucl  24043  injrec2  25222  ov2gc  25226  cur1val  25301  isprsr  25327  diophrw  26941  eldioph2  26944  diophren  26999  frlmup4  27356  psgnunilem1  27519  mendmulr  27599  trljco  31551  tgrpov  31559  tendovalco  31576  erngmul  31617  erngmul-rN  31625  cdlemksv  31655  cdlemkuu  31706  cdlemk41  31731  cdleml5N  31791  cdleml9  31795  dvamulr  31823  dvavadd  31826  dvhmulr  31898  dvhvscacbv  31910  dvhvscaval  31911  dih1dimatlem0  32140  dihjatcclem4  32233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-br 4040  df-opab 4094  df-co 4714
  Copyright terms: Public domain W3C validator