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

Theorem coeq1 5249
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 5247 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 coss1 5247 . . 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:  coeq1i  5251  coeq1d  5253  coi2  5621  relcnvtr  5624  funcoeqres  6134  ereq1  7709  domssex2  8080  wemapwe  8554  seqf1olem2  12797  seqf1o  12798  relexpsucnnl  13722  isps  17142  pwsco1mhm  17310  frmdup3  17344  symgov  17750  pmtr3ncom  17835  psgnunilem1  17853  frgpup3  18131  gsumval3  18248  evlseu  19456  evlsval2  19460  evls1val  19625  evls1sca  19628  evl1val  19633  mpfpf1  19655  pf1mpf  19656  pf1ind  19659  frgpcyg  19862  frlmup4  20080  xkococnlem  21402  xkococn  21403  cnmpt1k  21425  cnmptkk  21426  xkofvcn  21427  qtopeu  21459  qtophmeo  21560  utop2nei  21994  cncombf  23365  dgrcolem2  23968  dgrco  23969  motplusg  25371  hocsubdir  28532  hoddi  28737  opsqrlem1  28887  smatfval  29685  msubco  31189  trljco  35547  tgrpov  35555  tendovalco  35572  erngmul  35613  erngmul-rN  35621  cdlemksv  35651  cdlemkuu  35702  cdlemk41  35727  cdleml5N  35787  cdleml9  35791  dvamulr  35819  dvavadd  35822  dvhmulr  35894  dvhvscacbv  35906  dvhvscaval  35907  dih1dimatlem0  36136  dihjatcclem4  36229  diophrw  36841  eldioph2  36844  diophren  36896  mendmulr  37278  rngcinv  41299  rngcinvALTV  41311  ringcinv  41350  ringcinvALTV  41374
  Copyright terms: Public domain W3C validator