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

Theorem imaeq2d 5164
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 5160 . 2  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
31, 2syl 16 1  |-  ( ph  ->  ( C " A
)  =  ( C
" B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   "cima 4838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-opab 4346  df-xp 4841  df-cnv 4843  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848
This theorem is referenced by:  imaeq12d  5165  nfimad  5173  csbima12  5181  elimasng  5190  elimasni  5191  csbrn  5294  ressn  5368  foima  5620  f1imacnv  5652  dffv3  5682  fvco2  5761  fsn2  5878  funfvima3  5949  isofrlem  6026  isoselem  6027  fnexALT  6538  curry1  6659  curry2  6662  fparlem3  6669  fparlem4  6670  suppsnop  6699  ressuppssdif  6705  imacosupp  6724  eceq1  7129  uniqs2  7154  ecinxp  7167  mapsn  7246  sbthlem2  7414  sbth  7423  phplem4  7485  php3  7489  marypha1lem  7675  cantnffvalOLD  7863  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  wemapweOLD  7921  oef1oOLD  7923  tcrank  8083  fin4en1  8470  fin1a2lem7  8567  hsmexlem4  8590  hsmexlem5  8591  fpwwe2cbv  8789  fpwwe2lem3  8792  fpwwe2lem13  8801  fpwwecbv  8803  canth4  8806  frnnn0fsupp  10627  limsupgval  12946  isercoll  13137  vdwlem1  14034  vdwlem6  14039  vdwlem7  14040  vdwlem8  14041  vdwlem12  14045  vdwlem13  14046  vdwnn  14051  0ram  14073  ramz2  14077  isacs1i  14587  acsficl  15333  gsumvalx  15493  gsumpropd  15495  gsumpropd2lem  15496  gsumress  15498  efgrelexlema  16237  gsumval3a  16370  gsumval3aOLD  16371  gsumval3lem1  16374  gsumzsubmclOLD  16394  gsum2dlem2  16452  gsum2dOLD  16454  gsum2d2  16456  pwsgsumOLD  16464  dprdvalOLD  16477  dprddisj  16483  dprdf1o  16519  dprdsn  16523  dprd2dlem2  16529  dprd2dlem1  16530  dprd2da  16531  dprd2db  16532  dmdprdsplit2lem  16534  dpjfval  16544  coe1mul2lem2  17702  frlmgsumOLD  18175  frlmup3  18208  islindf  18221  islindf2  18223  lindfind  18225  f1lindf  18231  lmimlbs  18245  subbascn  18838  cncls2  18857  cncls  18858  cnntr  18859  cnpresti  18872  cnprest  18873  cnt1  18934  cnhaus  18938  cncmp  18975  cnconn  19006  1stcfb  19029  xkoccn  19172  ptrescn  19192  xkococnlem  19212  qtopeu  19269  qtoprest  19270  kqdisj  19285  kqcldsat  19286  ordthmeolem  19354  fmfnfmlem4  19510  ustuqtoplem  19794  utopsnneiplem  19802  utopsnneip  19803  ucncn  19840  metusttoOLD  20112  metustto  20113  metustexhalfOLD  20118  metustexhalf  20119  metustfbasOLD  20120  metustfbas  20121  cfilucfilOLD  20124  cfilucfil  20125  metuustOLD  20126  metuust  20127  cfilucfil2OLD  20128  cfilucfil2  20129  metuelOLD  20132  metuel  20133  metuel2  20134  metutopOLD  20137  psmetutop  20138  restmetu  20142  metucnOLD  20143  metucn  20144  pi1addval  20600  iscph  20669  uniioombllem3  21045  dyadmbl  21060  mbfima  21090  mbfimaicc  21091  mbfimasn  21092  ismbfd  21098  ismbf2d  21099  ismbf3d  21112  mbfimaopnlem  21113  i1fd  21139  i1f1  21148  itg11  21149  i1faddlem  21151  i1fmullem  21152  i1fadd  21153  itg1addlem3  21156  itg1mulc  21162  itg2gt0  21218  limcnlp  21333  ellimc3  21334  limcflf  21336  limciun  21349  mdegfvalOLD  21512  mdegval  21513  mdegvalOLD  21514  mdeg0  21521  mdegvsca  21527  mdegpropd  21535  deg1val  21547  ig1pval  21624  coeeu  21673  coeeq  21675  pserulm  21867  areambl  22332  spthispth  23440  1pthonlem2  23457  constr2pth  23468  constr3pthlem3  23511  eupath2lem3  23568  eupath2  23569  efghgrp  23828  issh  24578  isch  24593  shsval  24683  fimacnvinrn2  25921  sspreima  25930  dfcnv2  25962  zrhunitpreima  26376  mbfmco2  26649  sibfima  26693  sibfof  26695  eulerpartlemgv  26725  eulerpartlemn  26733  eulerpart  26734  orvcval4  26812  orvcelval  26820  orvcelel  26821  ballotlemscr  26870  erdszelem3  27050  erdsze  27059  cvmliftlem3  27145  cvmliftlem7  27149  cvmlift2lem9a  27161  opelco3  27558  nofulllem1  27812  nofulllem2  27813  funpartlem  27942  ptrest  28396  mblfinlem2  28400  volsupnfl  28407  itg2addnclem2  28415  tailval  28565  sstotbnd2  28644  ismtyhmeolem  28674  grpokerinj  28721  inisegn0  29367  dnnumch3lem  29370  aomclem8  29385  mapfien2OLD  29420  pwfi2f1o  29422  cytpval  29548  imarnf1pr  30121  usgra2pthspth  30266  usgra2adedglem1  30279  csbfv12gALTOLD  31486  lkrfval  32625
  Copyright terms: Public domain W3C validator