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

Theorem imaeq2d 5028
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 5024 . 2  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
31, 2syl 15 1  |-  ( ph  ->  ( C " A
)  =  ( C
" B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   "cima 4708
This theorem is referenced by:  imaeq12d  5029  nfimad  5037  elimasng  5055  elimasni  5056  ressn  5227  foima  5472  f1imacnv  5505  dffv3  5537  csbfv12gALT  5552  fvco2  5610  fsn2  5714  fnexALT  5758  funfvima3  5771  isofrlem  5853  isoselem  5854  curry1  6226  curry2  6229  fparlem3  6236  fparlem4  6237  eceq1  6712  uniqs2  6737  ecinxp  6750  mapsn  6825  sbthlem2  6988  sbth  6997  phplem4  7059  php3  7063  marypha1lem  7202  cantnfp1lem3  7398  wemapwe  7416  oef1o  7417  tcrank  7570  fin4en1  7951  fin1a2lem7  8048  hsmexlem4  8071  hsmexlem5  8072  fpwwe2cbv  8268  fpwwe2lem3  8271  fpwwe2lem13  8280  fpwwecbv  8282  canth4  8285  limsupgval  11966  isercoll  12157  vdwpc  13043  vdwlem1  13044  vdwlem6  13049  vdwlem7  13050  vdwlem8  13051  vdwlem12  13055  vdwlem13  13056  vdwnn  13061  0ram  13083  ramz2  13087  isacs1i  13575  acsficl  14290  gsumvalx  14467  gsumpropd  14469  gsumress  14470  efgrelexlema  15074  gsumval3a  15205  gsumzsubmcl  15216  gsum2d  15239  gsum2d2  15241  pwsgsum  15246  dmdprd  15252  dprdval  15254  dprddisj  15260  dprdf1o  15283  dprdsn  15287  dprd2dlem2  15291  dprd2dlem1  15292  dprd2da  15293  dprd2db  15294  dmdprdsplit2lem  15296  dpjfval  15306  isunit  15455  mplval  16189  ressmplbas2  16215  mplbaspropd  16330  coe1mul2lem2  16361  subbascn  17000  cncls2  17018  cncls  17019  cnntr  17020  cnpresti  17032  cnprest  17033  cnt1  17094  cnhaus  17098  cncmp  17135  cnconn  17164  1stcfb  17187  xkoccn  17329  ptrescn  17349  xkococnlem  17369  qtopval  17402  qtopeu  17423  qtoprest  17424  kqdisj  17439  kqcldsat  17440  ordthmeolem  17508  fmfnfmlem4  17668  pi1addval  18562  iscph  18622  uniioombllem3  18956  dyadmbl  18971  mbfima  19003  mbfimaicc  19004  mbfimasn  19005  ismbfd  19011  ismbf2d  19012  ismbf3d  19025  mbfimaopnlem  19026  i1fd  19052  i1f1  19061  itg11  19062  i1faddlem  19064  i1fmullem  19065  i1fadd  19066  itg1addlem3  19069  itg1mulc  19075  itg2gt0  19131  limcnlp  19244  ellimc3  19245  limcflf  19247  limciun  19260  mdegfval  19464  mdegval  19465  mdeg0  19472  mdegvsca  19478  mdegpropd  19486  ig1pval  19574  coeeu  19623  coeeq  19625  pserulm  19814  areambl  20269  efghgrp  21056  issh  21803  isch  21818  shsval  21907  ballotlemscr  23093  fimacnvinrn2  23215  sspreima  23225  gsumpropd2lem  23394  mbfmco2  23585  orvcval4  23676  orvcelval  23684  orvcelel  23685  erdszelem3  23739  erdsze  23748  cvmliftlem3  23833  cvmliftlem7  23837  cvmlift2lem9a  23849  eupath2lem3  23918  eupath2  23919  predeq3  24242  nofulllem1  24427  nofulllem2  24428  funpartlem  24552  itg2addnclem2  25004  nds  26253  tailval  26425  sstotbnd2  26601  ismtyhmeolem  26631  grpokerinj  26678  inisegn0  27243  dnnumch3lem  27246  aomclem8  27262  islmodfg  27270  frlmgsum  27335  uvcresum  27345  frlmup1  27353  frlmup3  27355  mapfien2  27361  pwfi2f1o  27363  islindf  27385  islindf2  27387  lindfind  27389  f1lindf  27395  lmimlbs  27409  cytpval  27631  spthispth  28359  constr3pthlem3  28403  lkrfval  29899
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-xp 4711  df-cnv 4713  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718
  Copyright terms: Public domain W3C validator