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

Theorem coeq1 5186
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 5184 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 coss1 5184 . . 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:  coeq1i  5188  coeq1d  5190  coi2  5552  relcnvtr  5555  funcoeqres  6062  ereq1  7610  domssex2  7979  wemapwe  8451  seqf1olem2  12655  seqf1o  12656  relexpsucnnl  13563  isps  16968  pwsco1mhm  17136  frmdup3  17170  symgov  17576  pmtr3ncom  17661  psgnunilem1  17679  frgpup3  17957  gsumval3  18074  evlseu  19280  evlsval2  19284  evls1val  19449  evls1sca  19452  evl1val  19457  mpfpf1  19479  pf1mpf  19480  pf1ind  19483  frgpcyg  19683  frlmup4  19898  xkococnlem  21211  xkococn  21212  cnmpt1k  21234  cnmptkk  21235  xkofvcn  21236  qtopeu  21268  qtophmeo  21369  utop2nei  21803  cncombf  23145  dgrcolem2  23748  dgrco  23749  motplusg  25152  hocsubdir  27831  hoddi  28036  opsqrlem1  28186  smatfval  28992  msubco  30485  trljco  34846  tgrpov  34854  tendovalco  34871  erngmul  34912  erngmul-rN  34920  cdlemksv  34950  cdlemkuu  35001  cdlemk41  35026  cdleml5N  35086  cdleml9  35090  dvamulr  35118  dvavadd  35121  dvhmulr  35193  dvhvscacbv  35205  dvhvscaval  35206  dih1dimatlem0  35435  dihjatcclem4  35528  diophrw  36140  eldioph2  36143  diophren  36195  mendmulr  36577  rngcinv  41772  rngcinvALTV  41784  ringcinv  41823  ringcinvALTV  41847
  Copyright terms: Public domain W3C validator