MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imaeq2d Structured version   Unicode version

Theorem imaeq2d 5195
Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
Hypothesis
Ref Expression
imaeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
imaeq2d  |-  ( ph  ->  ( C " A
)  =  ( C
" B ) )

Proof of Theorem imaeq2d
StepHypRef Expression
1 imaeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 imaeq2 5191 . 2  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
31, 2syl 16 1  |-  ( ph  ->  ( C " A
)  =  ( C
" B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   "cima 4873
This theorem is referenced by:  imaeq12d  5196  nfimad  5204  elimasng  5222  elimasni  5223  ressn  5400  foima  5650  f1imacnv  5683  dffv3  5716  csbfv12gALT  5731  fvco2  5790  fsn2  5900  fnexALT  5954  funfvima3  5967  isofrlem  6052  isoselem  6053  curry1  6430  curry2  6433  fparlem3  6440  fparlem4  6441  eceq1  6933  uniqs2  6958  ecinxp  6971  mapsn  7047  sbthlem2  7210  sbth  7219  phplem4  7281  php3  7285  marypha1lem  7430  cantnfp1lem3  7628  wemapwe  7646  oef1o  7647  tcrank  7800  fin4en1  8181  fin1a2lem7  8278  hsmexlem4  8301  hsmexlem5  8302  fpwwe2cbv  8497  fpwwe2lem3  8500  fpwwe2lem13  8509  fpwwecbv  8511  canth4  8514  limsupgval  12262  isercoll  12453  vdwlem1  13341  vdwlem6  13346  vdwlem7  13347  vdwlem8  13348  vdwlem12  13352  vdwlem13  13353  vdwnn  13358  0ram  13380  ramz2  13384  isacs1i  13874  acsficl  14589  gsumvalx  14766  gsumpropd  14768  gsumress  14769  efgrelexlema  15373  gsumval3a  15504  gsumzsubmcl  15515  gsum2d  15538  gsum2d2  15540  pwsgsum  15545  dprdval  15553  dprddisj  15559  dprdf1o  15582  dprdsn  15586  dprd2dlem2  15590  dprd2dlem1  15591  dprd2da  15592  dprd2db  15593  dmdprdsplit2lem  15595  dpjfval  15605  mplval  16484  ressmplbas2  16510  mplbaspropd  16622  coe1mul2lem2  16653  subbascn  17310  cncls2  17329  cncls  17330  cnntr  17331  cnpresti  17344  cnprest  17345  cnt1  17406  cnhaus  17410  cncmp  17447  cnconn  17477  1stcfb  17500  xkoccn  17643  ptrescn  17663  xkococnlem  17683  qtopeu  17740  qtoprest  17741  kqdisj  17756  kqcldsat  17757  ordthmeolem  17825  fmfnfmlem4  17981  ustuqtoplem  18261  utopsnneiplem  18269  utopsnneip  18270  ucncn  18307  metusttoOLD  18579  metustto  18580  metustexhalfOLD  18585  metustexhalf  18586  metustfbasOLD  18587  metustfbas  18588  cfilucfilOLD  18591  cfilucfil  18592  metuustOLD  18593  metuust  18594  cfilucfil2OLD  18595  cfilucfil2  18596  metuelOLD  18599  metuel  18600  metuel2  18601  metutopOLD  18604  psmetutop  18605  restmetu  18609  metucnOLD  18610  metucn  18611  pi1addval  19065  iscph  19125  uniioombllem3  19469  dyadmbl  19484  mbfima  19516  mbfimaicc  19517  mbfimasn  19518  ismbfd  19524  ismbf2d  19525  ismbf3d  19538  mbfimaopnlem  19539  i1fd  19565  i1f1  19574  itg11  19575  i1faddlem  19577  i1fmullem  19578  i1fadd  19579  itg1addlem3  19582  itg1mulc  19588  itg2gt0  19644  limcnlp  19757  ellimc3  19758  limcflf  19760  limciun  19773  mdegfval  19977  mdegval  19978  mdeg0  19985  mdegvsca  19991  mdegpropd  19999  ig1pval  20087  coeeu  20136  coeeq  20138  pserulm  20330  areambl  20789  spthispth  21565  1pthonlem2  21582  constr2pth  21593  constr3pthlem3  21636  eupath2lem3  21693  eupath2  21694  efghgrp  21953  issh  22702  isch  22717  shsval  22806  fimacnvinrn2  24040  sspreima  24049  gsumpropd2lem  24212  zrhunitpreima  24354  mbfmco2  24607  sibfima  24645  sibfof  24646  orvcval4  24710  orvcelval  24718  orvcelel  24719  ballotlemscr  24768  erdszelem3  24871  erdsze  24880  cvmliftlem3  24966  cvmliftlem7  24970  cvmlift2lem9a  24982  opelco3  25395  nofulllem1  25649  nofulllem2  25650  funpartlem  25779  mblfinlem  26234  volsupnfl  26241  itg2addnclem2  26247  tailval  26393  sstotbnd2  26474  ismtyhmeolem  26504  grpokerinj  26551  inisegn0  27109  dnnumch3lem  27112  aomclem8  27127  frlmgsum  27200  uvcresum  27210  frlmup1  27218  frlmup3  27220  mapfien2  27226  pwfi2f1o  27228  islindf  27250  islindf2  27252  lindfind  27254  f1lindf  27260  lmimlbs  27274  cytpval  27496  imarnf1pr  28070  usgra2pthspth  28258  usgra2adedglem1  28271  lkrfval  29822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-xp 4876  df-cnv 4878  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883
  Copyright terms: Public domain W3C validator