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

Theorem coeq1 5427
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 5425 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 coss1 5425 . . 3 (𝐵𝐴 → (𝐵𝐶) ⊆ (𝐴𝐶))
31, 2anim12i 591 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐴𝐶) ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ⊆ (𝐴𝐶)))
4 eqss 3751 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3751 . 2 ((𝐴𝐶) = (𝐵𝐶) ↔ ((𝐴𝐶) ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ⊆ (𝐴𝐶)))
63, 4, 53imtr4i 281 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1624  wss 3707  ccom 5262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-in 3714  df-ss 3721  df-br 4797  df-opab 4857  df-co 5267
This theorem is referenced by:  coeq1i  5429  coeq1d  5431  coi2  5805  relcnvtr  5808  funcoeqres  6320  ereq1  7910  domssex2  8277  wemapwe  8759  seqf1olem2  13027  seqf1o  13028  relexpsucnnl  13963  isps  17395  pwsco1mhm  17563  frmdup3  17597  symgov  18002  pmtr3ncom  18087  psgnunilem1  18105  frgpup3  18383  gsumval3  18500  evlseu  19710  evlsval2  19714  evls1val  19879  evls1sca  19882  evl1val  19887  mpfpf1  19909  pf1mpf  19910  pf1ind  19913  frgpcyg  20116  frlmup4  20334  xkococnlem  21656  xkococn  21657  cnmpt1k  21679  cnmptkk  21680  xkofvcn  21681  qtopeu  21713  qtophmeo  21814  utop2nei  22247  cncombf  23616  dgrcolem2  24221  dgrco  24222  motplusg  25628  hocsubdir  28945  hoddi  29150  opsqrlem1  29300  smatfval  30162  msubco  31727  coideq  34326  trljco  36522  tgrpov  36530  tendovalco  36547  erngmul  36588  erngmul-rN  36596  cdlemksv  36626  cdlemkuu  36677  cdlemk41  36702  cdleml5N  36762  cdleml9  36766  dvamulr  36794  dvavadd  36797  dvhmulr  36869  dvhvscacbv  36881  dvhvscaval  36882  dih1dimatlem0  37111  dihjatcclem4  37204  diophrw  37816  eldioph2  37819  diophren  37871  mendmulr  38252  rngcinv  42483  rngcinvALTV  42495  ringcinv  42534  ringcinvALTV  42558
  Copyright terms: Public domain W3C validator