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

Theorem imaeq2d 5012
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 5008 . 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 1623   "cima 4692
This theorem is referenced by:  imaeq12d  5013  nfimad  5021  elimasng  5039  elimasni  5040  ressn  5211  foima  5456  f1imacnv  5489  dffv3  5521  csbfv12gALT  5536  fvco2  5594  fsn2  5698  fnexALT  5742  funfvima3  5755  isofrlem  5837  isoselem  5838  curry1  6210  curry2  6213  fparlem3  6220  fparlem4  6221  eceq1  6696  uniqs2  6721  ecinxp  6734  mapsn  6809  sbthlem2  6972  sbth  6981  phplem4  7043  php3  7047  marypha1lem  7186  cantnfp1lem3  7382  wemapwe  7400  oef1o  7401  tcrank  7554  fin4en1  7935  fin1a2lem7  8032  hsmexlem4  8055  hsmexlem5  8056  fpwwe2cbv  8252  fpwwe2lem3  8255  fpwwe2lem13  8264  fpwwecbv  8266  canth4  8269  limsupgval  11950  isercoll  12141  vdwpc  13027  vdwlem1  13028  vdwlem6  13033  vdwlem7  13034  vdwlem8  13035  vdwlem12  13039  vdwlem13  13040  vdwnn  13045  0ram  13067  ramz2  13071  isacs1i  13559  acsficl  14274  gsumvalx  14451  gsumpropd  14453  gsumress  14454  efgrelexlema  15058  gsumval3a  15189  gsumzsubmcl  15200  gsum2d  15223  gsum2d2  15225  pwsgsum  15230  dmdprd  15236  dprdval  15238  dprddisj  15244  dprdf1o  15267  dprdsn  15271  dprd2dlem2  15275  dprd2dlem1  15276  dprd2da  15277  dprd2db  15278  dmdprdsplit2lem  15280  dpjfval  15290  isunit  15439  mplval  16173  ressmplbas2  16199  mplbaspropd  16314  coe1mul2lem2  16345  subbascn  16984  cncls2  17002  cncls  17003  cnntr  17004  cnpresti  17016  cnprest  17017  cnt1  17078  cnhaus  17082  cncmp  17119  cnconn  17148  1stcfb  17171  xkoccn  17313  ptrescn  17333  xkococnlem  17353  qtopval  17386  qtopeu  17407  qtoprest  17408  kqdisj  17423  kqcldsat  17424  ordthmeolem  17492  fmfnfmlem4  17652  pi1addval  18546  iscph  18606  uniioombllem3  18940  dyadmbl  18955  mbfima  18987  mbfimaicc  18988  mbfimasn  18989  ismbfd  18995  ismbf2d  18996  ismbf3d  19009  mbfimaopnlem  19010  i1fd  19036  i1f1  19045  itg11  19046  i1faddlem  19048  i1fmullem  19049  i1fadd  19050  itg1addlem3  19053  itg1mulc  19059  itg2gt0  19115  limcnlp  19228  ellimc3  19229  limcflf  19231  limciun  19244  mdegfval  19448  mdegval  19449  mdeg0  19456  mdegvsca  19462  mdegpropd  19470  ig1pval  19558  coeeu  19607  coeeq  19609  pserulm  19798  areambl  20253  efghgrp  21040  issh  21787  isch  21802  shsval  21891  ballotlemscr  23077  fimacnvinrn2  23200  sspreima  23210  gsumpropd2lem  23379  mbfmco2  23570  orvcval4  23661  orvcelval  23669  orvcelel  23670  erdszelem3  23724  erdsze  23733  cvmliftlem3  23818  cvmliftlem7  23822  cvmlift2lem9a  23834  eupath2lem3  23903  eupath2  23904  predeq3  24171  nofulllem1  24356  nofulllem2  24357  funpartfv  24483  nds  26150  tailval  26322  sstotbnd2  26498  ismtyhmeolem  26528  grpokerinj  26575  inisegn0  27140  dnnumch3lem  27143  aomclem8  27159  islmodfg  27167  frlmgsum  27232  uvcresum  27242  frlmup1  27250  frlmup3  27252  mapfien2  27258  pwfi2f1o  27260  islindf  27282  islindf2  27284  lindfind  27286  f1lindf  27292  lmimlbs  27306  cytpval  27528  lkrfval  29277
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702
  Copyright terms: Public domain W3C validator