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

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

Proof of Theorem coeq1
StepHypRef Expression
1 coss1 5812 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 coss1 5812 . . 3 (𝐵𝐴 → (𝐵𝐶) ⊆ (𝐴𝐶))
31, 2anim12i 614 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐴𝐶) ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ⊆ (𝐴𝐶)))
4 eqss 3960 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3960 . 2 ((𝐴𝐶) = (𝐵𝐶) ↔ ((𝐴𝐶) ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ⊆ (𝐴𝐶)))
63, 4, 53imtr4i 292 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wss 3911  ccom 5638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-co 5643
This theorem is referenced by:  coeq1i  5816  coeq1d  5818  coi2  6216  funcoeqres  6816  wrecseq123  8246  ereq1  8658  domssex2  9084  wemapwe  9638  dfttrcl2  9665  updjud  9875  seqf1olem2  13954  seqf1o  13955  relexpsucnnl  14921  isps  18462  pwsco1mhm  18647  frmdup3  18682  efmndov  18696  symggrplem  18699  smndex1mndlem  18724  smndex1mnd  18725  pmtr3ncom  19262  psgnunilem1  19280  frgpup3  19565  gsumval3  19689  frgpcyg  20996  frlmup4  21223  evlseu  21509  evlsval2  21513  selvval  21544  evls1val  21702  evls1sca  21705  evl1val  21711  mpfpf1  21733  pf1mpf  21734  pf1ind  21737  xkococnlem  23026  xkococn  23027  cnmpt1k  23049  cnmptkk  23050  xkofvcn  23051  qtopeu  23083  qtophmeo  23184  utop2nei  23618  cncombf  25038  dgrcolem2  25651  dgrco  25652  motplusg  27526  hocsubdir  30769  hoddi  30974  opsqrlem1  31124  smatfval  32433  msubco  34182  coideq  36750  trljco  39249  tgrpov  39257  tendovalco  39274  erngmul  39315  erngmul-rN  39323  cdlemksv  39353  cdlemkuu  39404  cdlemk41  39429  cdleml5N  39489  cdleml9  39493  dvamulr  39521  dvavadd  39524  dvhmulr  39595  dvhvscacbv  39607  dvhvscaval  39608  dih1dimatlem0  39837  dihjatcclem4  39930  evlsval3  40787  diophrw  41125  eldioph2  41128  diophren  41179  mendmulr  41558  fundcmpsurinjpreimafv  45686  rngcinv  46365  rngcinvALTV  46377  ringcinv  46416  ringcinvALTV  46440  itcoval  46833
  Copyright terms: Public domain W3C validator