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

Theorem coeq2 4879
Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
Assertion
Ref Expression
coeq2  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )

Proof of Theorem coeq2
StepHypRef Expression
1 coss2 4877 . . 3  |-  ( A 
C_  B  ->  ( C  o.  A )  C_  ( C  o.  B
) )
2 coss2 4877 . . 3  |-  ( B 
C_  A  ->  ( C  o.  B )  C_  ( C  o.  A
) )
31, 2anim12i 549 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( ( C  o.  A )  C_  ( C  o.  B )  /\  ( C  o.  B
)  C_  ( C  o.  A ) ) )
4 eqss 3228 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3228 . 2  |-  ( ( C  o.  A )  =  ( C  o.  B )  <->  ( ( C  o.  A )  C_  ( C  o.  B
)  /\  ( C  o.  B )  C_  ( C  o.  A )
) )
63, 4, 53imtr4i 257 1  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1633    C_ wss 3186    o. ccom 4730
This theorem is referenced by:  coeq2i  4881  coeq2d  4883  coi2  5226  relcnvtr  5229  relcoi1  5238  f1eqcocnv  5847  ereq1  6709  seqf1olem2  11133  seqf1o  11134  isps  14360  pwsco2mhm  14496  gsumwmhm  14516  frmdgsum  14533  frmdup1  14535  frmdup2  14536  symgov  14826  frgpuplem  15130  frgpupf  15131  frgpupval  15132  gsumval3eu  15239  gsumval3  15240  kgencn2  17308  upxp  17373  uptx  17375  txcn  17376  xkococnlem  17409  xkococn  17410  cnmptk1  17431  cnmptkk  17433  xkofvcn  17434  imasdsf1olem  17989  pi1cof  18610  pi1coval  18611  elovolmr  18888  ovoliunlem3  18916  ismbf1  19034  hocsubdir  22420  hoddi  22625  lnopco0i  22639  opsqrlem1  22775  pjsdi2i  22792  pjin2i  22828  pjclem1  22830  cvmliftmo  24099  cvmliftlem14  24112  cvmliftiota  24116  cvmlift2lem13  24130  cvmlift2  24131  cvmliftphtlem  24132  cvmlift3lem2  24135  cvmlift3lem6  24139  cvmlift3lem7  24140  cvmlift3lem9  24142  cvmlift3  24143  relexp0  24309  relexpsucr  24310  relexpsucl  24312  relexpadd  24319  upixp  25552  psgnunilem1  26564  mendmulr  26644  trlcoat  30730  trljco  30747  tgrpov  30755  tendovalco  30772  erngmul  30813  erngmul-rN  30821  dvamulr  31019  dvavadd  31022  dvhmulr  31094  dihjatcclem4  31429
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-in 3193  df-ss 3200  df-br 4061  df-opab 4115  df-co 4735
  Copyright terms: Public domain W3C validator