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

Theorem imaeq2d 5187
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 5183 . 2  |-  ( A  =  B  ->  ( C " A )  =  ( C " B
) )
31, 2syl 17 1  |-  ( ph  ->  ( C " A
)  =  ( C
" B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   "cima 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866
This theorem is referenced by:  imaeq12d  5188  nfimad  5196  csbima12  5204  elimasng  5213  elimasni  5214  inisegn0  5219  csbrn  5316  ressn  5391  foima  5815  f1imacnv  5847  dffv3  5877  fvco2  5956  fsn2  6077  funfvima3  6157  isofrlem  6246  isoselem  6247  fnexALT  6773  curry1  6899  curry2  6902  fparlem3  6909  fparlem4  6910  suppsnop  6939  ressuppssdif  6947  imacosupp  6966  eceq1  7410  uniqs2  7436  ecinxp  7449  mapsn  7524  sbthlem2  7692  sbth  7701  phplem4  7763  php3  7767  marypha1lem  7956  cantnfp1lem3  8193  tcrank  8363  fin4en1  8746  fin1a2lem7  8843  hsmexlem4  8866  hsmexlem5  8867  fpwwe2cbv  9062  fpwwe2lem3  9065  fpwwe2lem13  9074  fpwwecbv  9076  canth4  9079  frnnn0fsupp  10931  limsupgval  13533  isercoll  13730  vdwlem1  14930  vdwlem6  14935  vdwlem7  14936  vdwlem8  14937  vdwlem12  14941  vdwlem13  14942  vdwnn  14947  0ram  14977  ramz2  14981  isacs1i  15562  acsficl  16416  gsumvalx  16512  gsumpropd  16514  gsumpropd2lem  16515  gsumress  16518  efgrelexlema  17398  gsumval3a  17536  gsumval3lem1  17538  gsum2dlem2  17602  gsum2d2  17605  dprddisj  17640  dprdf1o  17664  dprdsn  17668  dprd2dlem2  17672  dprd2dlem1  17673  dprd2da  17674  dprd2db  17675  dmdprdsplit2lem  17677  dpjfval  17687  coe1mul2lem2  18860  frlmup3  19356  islindf  19368  islindf2  19370  lindfind  19372  f1lindf  19378  lmimlbs  19392  subbascn  20268  cncls2  20287  cncls  20288  cnntr  20289  cnpresti  20302  cnprest  20303  cnt1  20364  cnhaus  20368  cncmp  20405  cnconn  20435  1stcfb  20458  xkoccn  20632  ptrescn  20652  xkococnlem  20672  qtopeu  20729  qtoprest  20730  kqdisj  20745  kqcldsat  20746  ordthmeolem  20814  fmfnfmlem4  20970  ustuqtoplem  21252  utopsnneiplem  21260  utopsnneip  21261  ucncn  21298  metustto  21566  metustexhalf  21569  metustfbas  21570  cfilucfil  21572  metuust  21573  cfilucfil2  21574  metuel  21577  metuel2  21578  psmetutop  21580  restmetu  21583  metucn  21584  pi1addval  22077  iscph  22146  uniioombllem3  22541  dyadmbl  22556  mbfima  22586  mbfimaicc  22587  mbfimasn  22588  ismbfd  22594  ismbf2d  22595  ismbf3d  22608  mbfimaopnlem  22609  i1fd  22637  i1f1  22646  itg11  22647  i1faddlem  22649  i1fmullem  22650  i1fadd  22651  itg1addlem3  22654  itg1mulc  22660  itg2gt0  22716  limcnlp  22831  ellimc3  22832  limcflf  22834  limciun  22847  mdegval  23010  mdeg0  23017  mdegvsca  23023  mdegpropd  23031  deg1val  23043  ig1pval  23122  ig1pvalOLD  23128  coeeu  23177  coeeq  23179  pserulm  23375  areambl  23882  spthispth  25301  1pthonlem2  25318  constr2pth  25329  constr3pthlem3  25383  eupath2lem3  25705  eupath2  25706  efghgrpOLD  26099  issh  26859  isch  26873  shsval  26963  fimacnvinrn2  28238  sspreima  28248  dfcnv2  28281  gsummpt2co  28550  smatrcl  28630  locfinreflem  28675  zrhunitpreima  28790  mbfmco2  29095  sibfima  29179  sibfof  29181  eulerpartlemgv  29214  eulerpartlemn  29222  eulerpart  29223  orvcval4  29301  orvcelval  29309  orvcelel  29310  ballotlemscr  29359  ballotlemscrOLD  29397  erdszelem3  29924  erdsze  29933  cvmliftlem3  30018  cvmliftlem7  30022  cvmlift2lem9a  30034  msrval  30184  mvtinf  30201  mclsval  30209  mclsax  30215  mthmpps  30228  opelco3  30427  nofulllem1  30596  nofulllem2  30597  funpartlem  30714  tailval  31034  csbpredg  31691  ptrest  31903  poimirlem1  31905  poimirlem2  31906  poimirlem3  31907  poimirlem4  31908  poimirlem5  31909  poimirlem6  31910  poimirlem7  31911  poimirlem9  31913  poimirlem10  31914  poimirlem11  31915  poimirlem12  31916  poimirlem13  31917  poimirlem14  31918  poimirlem15  31919  poimirlem16  31920  poimirlem17  31921  poimirlem19  31923  poimirlem20  31924  poimirlem22  31926  poimirlem23  31927  poimirlem24  31928  poimirlem25  31929  poimirlem26  31930  poimirlem27  31931  poimirlem28  31932  poimirlem29  31933  poimirlem31  31935  poimirlem32  31936  mblfinlem2  31942  volsupnfl  31949  itg2addnclem2  31958  sstotbnd2  32070  ismtyhmeolem  32100  grpokerinj  32147  lkrfval  32622  dnnumch3lem  35874  aomclem8  35889  pwfi2f1o  35924  cytpval  36056  frege97d  36314  frege109d  36319  frege131d  36326  nzprmdif  36638  csbfv12gALTOLD  37186  wessf1ornlem  37420  imarnf1pr  38879  usgra2pthspth  39285  usgra2adedglem1  39290
  Copyright terms: Public domain W3C validator