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

Theorem coeq2 5250
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 5248 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 coss2 5248 . . 3 (𝐵𝐴 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2anim12i 589 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
4 eqss 3603 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3603 . 2 ((𝐶𝐴) = (𝐶𝐵) ↔ ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
63, 4, 53imtr4i 281 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wss 3560  ccom 5088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-in 3567  df-ss 3574  df-br 4624  df-opab 4684  df-co 5093
This theorem is referenced by:  coeq2i  5252  coeq2d  5254  coi2  5621  relcnvtr  5624  f1eqcocnv  6521  ereq1  7709  seqf1olem2  12797  seqf1o  12798  relexpsucnnr  13715  isps  17142  pwsco2mhm  17311  gsumwmhm  17322  frmdgsum  17339  frmdup1  17341  frmdup2  17342  symgov  17750  pmtr3ncom  17835  psgnunilem1  17853  frgpuplem  18125  frgpupf  18126  frgpupval  18127  gsumval3eu  18245  gsumval3lem2  18247  kgencn2  21300  upxp  21366  uptx  21368  txcn  21369  xkococnlem  21402  xkococn  21403  cnmptk1  21424  cnmptkk  21426  xkofvcn  21427  imasdsf1olem  22118  pi1cof  22799  pi1coval  22800  elovolmr  23184  ovoliunlem3  23212  ismbf1  23333  motplusg  25371  hocsubdir  28532  hoddi  28737  lnopco0i  28751  opsqrlem1  28887  pjsdi2i  28904  pjin2i  28940  pjclem1  28942  symgfcoeu  29672  eulerpartgbij  30257  cvmliftmo  31027  cvmliftlem14  31040  cvmliftiota  31044  cvmlift2lem13  31058  cvmlift2  31059  cvmliftphtlem  31060  cvmlift3lem2  31063  cvmlift3lem6  31067  cvmlift3lem7  31068  cvmlift3lem9  31070  cvmlift3  31071  msubco  31189  ftc1anclem8  33163  upixp  33195  trlcoat  35530  trljco  35547  tgrpov  35555  tendovalco  35572  erngmul  35613  erngmul-rN  35621  dvamulr  35819  dvavadd  35822  dvhmulr  35894  dihjatcclem4  36229  mendmulr  37278  hoiprodcl2  40106  ovnlecvr  40109  ovncvrrp  40115  ovnsubaddlem2  40122  ovncvr2  40162  opnvonmbllem1  40183  opnvonmbl  40185  ovolval4lem2  40201  ovolval5lem2  40204  ovolval5lem3  40205  ovolval5  40206  ovnovollem2  40208  rngcinv  41299  rngcinvALTV  41311  ringcinv  41350  ringcinvALTV  41374
  Copyright terms: Public domain W3C validator