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

Theorem coeq2 5187
Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
Assertion
Ref Expression
coeq2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem coeq2
StepHypRef Expression
1 coss2 5185 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 coss2 5185 . . 3 (𝐵𝐴 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2anim12i 587 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
4 eqss 3579 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3579 . 2 ((𝐶𝐴) = (𝐶𝐵) ↔ ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
63, 4, 53imtr4i 279 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wss 3536  ccom 5029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-in 3543  df-ss 3550  df-br 4575  df-opab 4635  df-co 5034
This theorem is referenced by:  coeq2i  5189  coeq2d  5191  coi2  5552  relcnvtr  5555  f1eqcocnv  6431  ereq1  7610  seqf1olem2  12655  seqf1o  12656  relexpsucnnr  13556  isps  16968  pwsco2mhm  17137  gsumwmhm  17148  frmdgsum  17165  frmdup1  17167  frmdup2  17168  symgov  17576  pmtr3ncom  17661  psgnunilem1  17679  frgpuplem  17951  frgpupf  17952  frgpupval  17953  gsumval3eu  18071  gsumval3lem2  18073  kgencn2  21109  upxp  21175  uptx  21177  txcn  21178  xkococnlem  21211  xkococn  21212  cnmptk1  21233  cnmptkk  21235  xkofvcn  21236  imasdsf1olem  21926  pi1cof  22595  pi1coval  22596  elovolmr  22965  ovoliunlem3  22993  ismbf1  23113  motplusg  25152  hocsubdir  27831  hoddi  28036  lnopco0i  28050  opsqrlem1  28186  pjsdi2i  28203  pjin2i  28239  pjclem1  28241  symgfcoeu  28979  eulerpartgbij  29564  cvmliftmo  30323  cvmliftlem14  30336  cvmliftiota  30340  cvmlift2lem13  30354  cvmlift2  30355  cvmliftphtlem  30356  cvmlift3lem2  30359  cvmlift3lem6  30363  cvmlift3lem7  30364  cvmlift3lem9  30366  cvmlift3  30367  msubco  30485  ftc1anclem8  32462  upixp  32494  trlcoat  34829  trljco  34846  tgrpov  34854  tendovalco  34871  erngmul  34912  erngmul-rN  34920  dvamulr  35118  dvavadd  35121  dvhmulr  35193  dihjatcclem4  35528  mendmulr  36577  hoiprodcl2  39246  ovnlecvr  39249  ovncvrrp  39255  ovnsubaddlem2  39262  ovncvr2  39302  opnvonmbllem1  39323  opnvonmbl  39325  ovolval4lem2  39341  ovolval5lem2  39344  ovolval5lem3  39345  ovolval5  39346  ovnovollem2  39348  rngcinv  41772  rngcinvALTV  41784  ringcinv  41823  ringcinvALTV  41847
  Copyright terms: Public domain W3C validator