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

Theorem coeq2d 5392
Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
Hypothesis
Ref Expression
coeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
coeq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem coeq2d
StepHypRef Expression
1 coeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 coeq2 5388 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596  ccom 5222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-in 3687  df-ss 3694  df-br 4761  df-opab 4821  df-co 5227
This theorem is referenced by:  coeq12d  5394  f1ococnv1  6278  funcoeqres  6280  fcof1oinvd  6663  foeqcnvco  6670  fparlem3  7399  fparlem4  7400  mapen  8240  mapfien  8429  wemapwe  8707  hashfacen  13351  s1co  13700  relexpsucnnl  13892  relexpsucl  13893  relexpcnv  13895  relexpaddnn  13911  relexpaddg  13913  prdsval  16238  isofval  16539  cofuass  16671  cofurid  16673  fucid  16753  setcinv  16862  catcisolem  16878  curf2ndf  17009  pwsco2mhm  17493  symggrp  17941  f1omvdco2  17989  psgnunilem1  18034  efginvrel2  18261  efginvrel1  18262  vrgpinv  18303  frgpuplem  18306  gsumval3  18429  gsumzf1o  18434  psrass1lem  19500  mpfrcl  19641  evlsval  19642  evls1fval  19807  evl1fval  19815  pf1mpf  19839  pf1ind  19842  ofco2  20380  qtophmeo  21743  ustssco  22140  utop2nei  22176  neipcfilu  22222  tngds  22574  elovolmr  23365  ovoliunlem3  23393  uniioombllem2  23472  hoddi  29079  fcoinver  29646  fmptco1f1o  29664  fcobij  29730  symgfcoeu  30075  smatfval  30091  eulerpartlemgv  30665  eulerpartlemn  30673  eulerpart  30674  sseqval  30680  reprpmtf1o  30934  erdsze2lem2  31414  cvmliftlem10  31504  mrsubval  31634  dfpo2  31873  ftc1anclem8  33724  cocnv  33752  ltrncoidN  35834  trlcoabs2N  36429  cdlemg47a  36441  cdlemg46  36442  cdlemg47  36443  ltrnco4  36446  tendovalco  36472  tendoplcbv  36482  tendopl  36483  tendoplass  36490  cdlemi2  36526  cdlemk2  36539  cdlemk4  36541  cdlemk8  36545  cdlemkuu  36602  cdlemk53  36664  cdlemk54  36665  cdlemk55a  36666  erngdvlem3  36697  erngdvlem3-rN  36705  tendocnv  36729  tendospcanN  36731  dvhvaddcbv  36797  dvhvaddval  36798  dvhvaddass  36805  dvhvscacbv  36806  dvhvscaval  36807  dvhopvsca  36810  dvhlveclem  36816  dvhopspN  36823  diblss  36878  cdlemn8  36912  dihopelvalcpre  36956  dihmeetlem1N  36998  dihglblem5apreN  36999  dih1dimatlem0  37036  dihjatcclem4  37129  diophrw  37741  eldioph2  37744  relexpaddss  38429  trclfvcom  38434  frege131d  38475  fsovrfovd  38722  hoicvrrex  41193  ovnlecvr  41195  ovncvrrp  41201  ovn0lem  41202  ovnsubaddlem1  41207  ovnsubadd  41209  ovnhoilem1  41238  ovnhoi  41240  ovnlecvr2  41247  ovncvr2  41248  hspmbl  41266  ovnovollem1  41293  ovnovollem3  41295  pfxco  41865
  Copyright terms: Public domain W3C validator