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

Theorem imaeq2d 5188
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 5184 . 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 4857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-xp 4860  df-cnv 4862  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867
This theorem is referenced by:  imaeq12d  5189  nfimad  5197  csbima12  5205  elimasng  5214  elimasni  5215  inisegn0  5220  csbrn  5317  ressn  5392  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  7407  uniqs2  7433  ecinxp  7446  mapsn  7521  sbthlem2  7689  sbth  7698  phplem4  7760  php3  7764  marypha1lem  7953  cantnfp1lem3  8184  tcrank  8354  fin4en1  8737  fin1a2lem7  8834  hsmexlem4  8857  hsmexlem5  8858  fpwwe2cbv  9054  fpwwe2lem3  9057  fpwwe2lem13  9066  fpwwecbv  9068  canth4  9071  frnnn0fsupp  10924  limsupgval  13512  isercoll  13709  vdwlem1  14894  vdwlem6  14899  vdwlem7  14900  vdwlem8  14901  vdwlem12  14905  vdwlem13  14906  vdwnn  14911  0ram  14941  ramz2  14945  isacs1i  15514  acsficl  16368  gsumvalx  16464  gsumpropd  16466  gsumpropd2lem  16467  gsumress  16470  efgrelexlema  17334  gsumval3a  17472  gsumval3lem1  17474  gsum2dlem2  17538  gsum2d2  17541  dprddisj  17576  dprdf1o  17600  dprdsn  17604  dprd2dlem2  17608  dprd2dlem1  17609  dprd2da  17610  dprd2db  17611  dmdprdsplit2lem  17613  dpjfval  17623  coe1mul2lem2  18796  frlmup3  19289  islindf  19301  islindf2  19303  lindfind  19305  f1lindf  19311  lmimlbs  19325  subbascn  20201  cncls2  20220  cncls  20221  cnntr  20222  cnpresti  20235  cnprest  20236  cnt1  20297  cnhaus  20301  cncmp  20338  cnconn  20368  1stcfb  20391  xkoccn  20565  ptrescn  20585  xkococnlem  20605  qtopeu  20662  qtoprest  20663  kqdisj  20678  kqcldsat  20679  ordthmeolem  20747  fmfnfmlem4  20903  ustuqtoplem  21185  utopsnneiplem  21193  utopsnneip  21194  ucncn  21231  metustto  21499  metustexhalf  21502  metustfbas  21503  cfilucfil  21505  metuust  21506  cfilucfil2  21507  metuel  21510  metuel2  21511  psmetutop  21513  restmetu  21516  metucn  21517  pi1addval  21972  iscph  22041  uniioombllem3  22420  dyadmbl  22435  mbfima  22465  mbfimaicc  22466  mbfimasn  22467  ismbfd  22473  ismbf2d  22474  ismbf3d  22487  mbfimaopnlem  22488  i1fd  22516  i1f1  22525  itg11  22526  i1faddlem  22528  i1fmullem  22529  i1fadd  22530  itg1addlem3  22533  itg1mulc  22539  itg2gt0  22595  limcnlp  22710  ellimc3  22711  limcflf  22713  limciun  22726  mdegval  22889  mdeg0  22896  mdegvsca  22902  mdegpropd  22910  deg1val  22922  ig1pval  22998  coeeu  23047  coeeq  23049  pserulm  23242  areambl  23749  spthispth  25148  1pthonlem2  25165  constr2pth  25176  constr3pthlem3  25230  eupath2lem3  25552  eupath2  25553  efghgrpOLD  25946  issh  26696  isch  26710  shsval  26800  fimacnvinrn2  28076  sspreima  28086  dfcnv2  28119  gsummpt2co  28381  smatrcl  28461  locfinreflem  28506  zrhunitpreima  28621  mbfmco2  28926  sibfima  28999  sibfof  29001  eulerpartlemgv  29032  eulerpartlemn  29040  eulerpart  29041  orvcval4  29119  orvcelval  29127  orvcelel  29128  ballotlemscr  29177  erdszelem3  29704  erdsze  29713  cvmliftlem3  29798  cvmliftlem7  29802  cvmlift2lem9a  29814  msrval  29964  mvtinf  29981  mclsval  29989  mclsax  29995  mthmpps  30008  opelco3  30207  nofulllem1  30376  nofulllem2  30377  funpartlem  30494  tailval  30814  ptrest  31643  poimirlem1  31645  poimirlem2  31646  poimirlem3  31647  poimirlem4  31648  poimirlem5  31649  poimirlem6  31650  poimirlem7  31651  poimirlem9  31653  poimirlem10  31654  poimirlem11  31655  poimirlem12  31656  poimirlem13  31657  poimirlem14  31658  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem22  31666  poimirlem23  31667  poimirlem24  31668  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  poimirlem29  31673  poimirlem31  31675  poimirlem32  31676  mblfinlem2  31682  volsupnfl  31689  itg2addnclem2  31698  sstotbnd2  31810  ismtyhmeolem  31840  grpokerinj  31887  lkrfval  32362  dnnumch3lem  35610  aomclem8  35625  pwfi2f1o  35660  cytpval  35785  frege97d  35983  frege109d  35988  frege131d  35995  nzprmdif  36305  csbfv12gALTOLD  36853  wessf1ornlem  37082  imarnf1pr  38386  usgra2pthspth  38421  usgra2adedglem1  38426
  Copyright terms: Public domain W3C validator