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

Theorem coeq1 5696
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 5694 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 coss1 5694 . . 3 (𝐵𝐴 → (𝐵𝐶) ⊆ (𝐴𝐶))
31, 2anim12i 615 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐴𝐶) ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ⊆ (𝐴𝐶)))
4 eqss 3933 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3933 . 2 ((𝐴𝐶) = (𝐵𝐶) ↔ ((𝐴𝐶) ⊆ (𝐵𝐶) ∧ (𝐵𝐶) ⊆ (𝐴𝐶)))
63, 4, 53imtr4i 295 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wss 3884  ccom 5527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-br 5034  df-opab 5096  df-co 5532
This theorem is referenced by:  coeq1i  5698  coeq1d  5700  coi2  6087  funcoeqres  6624  ereq1  8283  domssex2  8665  wemapwe  9148  updjud  9351  seqf1olem2  13410  seqf1o  13411  relexpsucnnl  14385  isps  17808  pwsco1mhm  17992  frmdup3  18028  efmndov  18042  symggrplem  18045  smndex1mndlem  18070  smndex1mnd  18071  pmtr3ncom  18599  psgnunilem1  18617  frgpup3  18900  gsumval3  19024  frgpcyg  20269  frlmup4  20494  evlseu  20759  evlsval2  20763  selvval  20794  evls1val  20948  evls1sca  20951  evl1val  20957  mpfpf1  20979  pf1mpf  20980  pf1ind  20983  xkococnlem  22268  xkococn  22269  cnmpt1k  22291  cnmptkk  22292  xkofvcn  22293  qtopeu  22325  qtophmeo  22426  utop2nei  22860  cncombf  24266  dgrcolem2  24875  dgrco  24876  motplusg  26340  hocsubdir  29572  hoddi  29777  opsqrlem1  29927  smatfval  31152  msubco  32892  coideq  35666  trljco  38035  tgrpov  38043  tendovalco  38060  erngmul  38101  erngmul-rN  38109  cdlemksv  38139  cdlemkuu  38190  cdlemk41  38215  cdleml5N  38275  cdleml9  38279  dvamulr  38307  dvavadd  38310  dvhmulr  38381  dvhvscacbv  38393  dvhvscaval  38394  dih1dimatlem0  38623  dihjatcclem4  38716  diophrw  39693  eldioph2  39696  diophren  39747  mendmulr  40125  fundcmpsurinjpreimafv  43918  rngcinv  44598  rngcinvALTV  44610  ringcinv  44649  ringcinvALTV  44673  itcoval  45068
  Copyright terms: Public domain W3C validator