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

Theorem imaeq2d 5325
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 5321 . 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 1398   "cima 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-xp 4994  df-cnv 4996  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001
This theorem is referenced by:  imaeq12d  5326  nfimad  5334  csbima12  5342  elimasng  5351  elimasni  5352  csbrn  5452  ressn  5526  foima  5782  f1imacnv  5814  dffv3  5844  fvco2  5923  fsn2  6047  funfvima3  6124  isofrlem  6211  isoselem  6212  fnexALT  6739  curry1  6865  curry2  6868  fparlem3  6875  fparlem4  6876  suppsnop  6905  ressuppssdif  6913  imacosupp  6932  eceq1  7339  uniqs2  7365  ecinxp  7378  mapsn  7453  sbthlem2  7621  sbth  7630  phplem4  7692  php3  7696  marypha1lem  7885  cantnffvalOLD  8073  cantnfp1lem3  8090  cantnfp1lem3OLD  8116  wemapweOLD  8131  oef1oOLD  8133  tcrank  8293  fin4en1  8680  fin1a2lem7  8777  hsmexlem4  8800  hsmexlem5  8801  fpwwe2cbv  8997  fpwwe2lem3  9000  fpwwe2lem13  9009  fpwwecbv  9011  canth4  9014  frnnn0fsupp  10847  limsupgval  13381  isercoll  13572  vdwlem1  14583  vdwlem6  14588  vdwlem7  14589  vdwlem8  14590  vdwlem12  14594  vdwlem13  14595  vdwnn  14600  0ram  14622  ramz2  14626  isacs1i  15146  acsficl  16000  gsumvalx  16096  gsumpropd  16098  gsumpropd2lem  16099  gsumress  16102  efgrelexlema  16966  gsumval3a  17104  gsumval3aOLD  17105  gsumval3lem1  17108  gsumzsubmclOLD  17128  gsum2dlem2  17194  gsum2dOLD  17196  gsum2d2  17198  pwsgsumOLD  17205  dprdvalOLD  17231  dprddisj  17237  dprdf1o  17274  dprdsn  17278  dprd2dlem2  17284  dprd2dlem1  17285  dprd2da  17286  dprd2db  17287  dmdprdsplit2lem  17289  dpjfval  17299  coe1mul2lem2  18504  frlmgsumOLD  18972  frlmup3  19002  islindf  19014  islindf2  19016  lindfind  19018  f1lindf  19024  lmimlbs  19038  subbascn  19922  cncls2  19941  cncls  19942  cnntr  19943  cnpresti  19956  cnprest  19957  cnt1  20018  cnhaus  20022  cncmp  20059  cnconn  20089  1stcfb  20112  xkoccn  20286  ptrescn  20306  xkococnlem  20326  qtopeu  20383  qtoprest  20384  kqdisj  20399  kqcldsat  20400  ordthmeolem  20468  fmfnfmlem4  20624  ustuqtoplem  20908  utopsnneiplem  20916  utopsnneip  20917  ucncn  20954  metusttoOLD  21226  metustto  21227  metustexhalfOLD  21232  metustexhalf  21233  metustfbasOLD  21234  metustfbas  21235  cfilucfilOLD  21238  cfilucfil  21239  metuustOLD  21240  metuust  21241  cfilucfil2OLD  21242  cfilucfil2  21243  metuelOLD  21246  metuel  21247  metuel2  21248  metutopOLD  21251  psmetutop  21252  restmetu  21256  metucnOLD  21257  metucn  21258  pi1addval  21714  iscph  21783  uniioombllem3  22160  dyadmbl  22175  mbfima  22205  mbfimaicc  22206  mbfimasn  22207  ismbfd  22213  ismbf2d  22214  ismbf3d  22227  mbfimaopnlem  22228  i1fd  22254  i1f1  22263  itg11  22264  i1faddlem  22266  i1fmullem  22267  i1fadd  22268  itg1addlem3  22271  itg1mulc  22277  itg2gt0  22333  limcnlp  22448  ellimc3  22449  limcflf  22451  limciun  22464  mdegfvalOLD  22627  mdegval  22628  mdegvalOLD  22629  mdeg0  22636  mdegvsca  22642  mdegpropd  22650  deg1val  22662  ig1pval  22739  coeeu  22788  coeeq  22790  pserulm  22983  areambl  23486  spthispth  24777  1pthonlem2  24794  constr2pth  24805  constr3pthlem3  24859  eupath2lem3  25181  eupath2  25182  efghgrpOLD  25573  issh  26323  isch  26338  shsval  26428  fimacnvinrn2  27697  sspreima  27706  dfcnv2  27745  gsummpt2co  28005  locfinreflem  28078  zrhunitpreima  28193  mbfmco2  28473  sibfima  28544  sibfof  28546  eulerpartlemgv  28576  eulerpartlemn  28584  eulerpart  28585  orvcval4  28663  orvcelval  28671  orvcelel  28672  ballotlemscr  28721  erdszelem3  28901  erdsze  28910  cvmliftlem3  28996  cvmliftlem7  29000  cvmlift2lem9a  29012  msrval  29162  mvtinf  29179  mclsval  29187  mclsax  29193  mthmpps  29206  opelco3  29448  nofulllem1  29702  nofulllem2  29703  funpartlem  29820  ptrest  30288  mblfinlem2  30292  volsupnfl  30299  itg2addnclem2  30307  tailval  30431  sstotbnd2  30510  ismtyhmeolem  30540  grpokerinj  30587  inisegn0  31228  dnnumch3lem  31231  aomclem8  31246  mapfien2OLD  31281  pwfi2f1o  31283  pwfi2f1oOLD  31284  cytpval  31410  nzprmdif  31465  imarnf1pr  32683  usgra2pthspth  32723  usgra2adedglem1  32728  csbfv12gALTOLD  34017  lkrfval  35209
  Copyright terms: Public domain W3C validator