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

Theorem imaeq2d 5337
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 5333 . 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 1379   "cima 5002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012
This theorem is referenced by:  imaeq12d  5338  nfimad  5346  csbima12  5354  elimasng  5363  elimasni  5364  csbrn  5468  ressn  5543  foima  5800  f1imacnv  5832  dffv3  5862  fvco2  5942  fsn2  6061  funfvima3  6137  isofrlem  6224  isoselem  6225  fnexALT  6750  curry1  6875  curry2  6878  fparlem3  6885  fparlem4  6886  suppsnop  6915  ressuppssdif  6921  imacosupp  6940  eceq1  7347  uniqs2  7373  ecinxp  7386  mapsn  7460  sbthlem2  7628  sbth  7637  phplem4  7699  php3  7703  marypha1lem  7893  cantnffvalOLD  8082  cantnfp1lem3  8099  cantnfp1lem3OLD  8125  wemapweOLD  8140  oef1oOLD  8142  tcrank  8302  fin4en1  8689  fin1a2lem7  8786  hsmexlem4  8809  hsmexlem5  8810  fpwwe2cbv  9008  fpwwe2lem3  9011  fpwwe2lem13  9020  fpwwecbv  9022  canth4  9025  frnnn0fsupp  10851  limsupgval  13262  isercoll  13453  vdwlem1  14358  vdwlem6  14363  vdwlem7  14364  vdwlem8  14365  vdwlem12  14369  vdwlem13  14370  vdwnn  14375  0ram  14397  ramz2  14401  isacs1i  14912  acsficl  15658  gsumvalx  15824  gsumpropd  15826  gsumpropd2lem  15827  gsumress  15829  efgrelexlema  16573  gsumval3a  16708  gsumval3aOLD  16709  gsumval3lem1  16712  gsumzsubmclOLD  16732  gsum2dlem2  16801  gsum2dOLD  16803  gsum2d2  16805  pwsgsumOLD  16813  dprdvalOLD  16839  dprddisj  16845  dprdf1o  16881  dprdsn  16885  dprd2dlem2  16891  dprd2dlem1  16892  dprd2da  16893  dprd2db  16894  dmdprdsplit2lem  16896  dpjfval  16906  coe1mul2lem2  18108  frlmgsumOLD  18596  frlmup3  18629  islindf  18642  islindf2  18644  lindfind  18646  f1lindf  18652  lmimlbs  18666  subbascn  19549  cncls2  19568  cncls  19569  cnntr  19570  cnpresti  19583  cnprest  19584  cnt1  19645  cnhaus  19649  cncmp  19686  cnconn  19717  1stcfb  19740  xkoccn  19883  ptrescn  19903  xkococnlem  19923  qtopeu  19980  qtoprest  19981  kqdisj  19996  kqcldsat  19997  ordthmeolem  20065  fmfnfmlem4  20221  ustuqtoplem  20505  utopsnneiplem  20513  utopsnneip  20514  ucncn  20551  metusttoOLD  20823  metustto  20824  metustexhalfOLD  20829  metustexhalf  20830  metustfbasOLD  20831  metustfbas  20832  cfilucfilOLD  20835  cfilucfil  20836  metuustOLD  20837  metuust  20838  cfilucfil2OLD  20839  cfilucfil2  20840  metuelOLD  20843  metuel  20844  metuel2  20845  metutopOLD  20848  psmetutop  20849  restmetu  20853  metucnOLD  20854  metucn  20855  pi1addval  21311  iscph  21380  uniioombllem3  21757  dyadmbl  21772  mbfima  21802  mbfimaicc  21803  mbfimasn  21804  ismbfd  21810  ismbf2d  21811  ismbf3d  21824  mbfimaopnlem  21825  i1fd  21851  i1f1  21860  itg11  21861  i1faddlem  21863  i1fmullem  21864  i1fadd  21865  itg1addlem3  21868  itg1mulc  21874  itg2gt0  21930  limcnlp  22045  ellimc3  22046  limcflf  22048  limciun  22061  mdegfvalOLD  22224  mdegval  22225  mdegvalOLD  22226  mdeg0  22233  mdegvsca  22239  mdegpropd  22247  deg1val  22259  ig1pval  22336  coeeu  22385  coeeq  22387  pserulm  22579  areambl  23044  spthispth  24279  1pthonlem2  24296  constr2pth  24307  constr3pthlem3  24361  eupath2lem3  24683  eupath2  24684  efghgrp  25079  issh  25829  isch  25844  shsval  25934  fimacnvinrn2  27177  sspreima  27185  dfcnv2  27217  zrhunitpreima  27623  mbfmco2  27904  sibfima  27948  sibfof  27950  eulerpartlemgv  27980  eulerpartlemn  27988  eulerpart  27989  orvcval4  28067  orvcelval  28075  orvcelel  28076  ballotlemscr  28125  erdszelem3  28305  erdsze  28314  cvmliftlem3  28400  cvmliftlem7  28404  cvmlift2lem9a  28416  opelco3  28813  nofulllem1  29067  nofulllem2  29068  funpartlem  29197  ptrest  29653  mblfinlem2  29657  volsupnfl  29664  itg2addnclem2  29672  tailval  29822  sstotbnd2  29901  ismtyhmeolem  29931  grpokerinj  29978  inisegn0  30621  dnnumch3lem  30624  aomclem8  30639  mapfien2OLD  30674  pwfi2f1o  30676  cytpval  30802  nzprmdif  30852  imarnf1pr  31804  usgra2pthspth  31846  usgra2adedglem1  31851  csbfv12gALTOLD  32719  lkrfval  33902
  Copyright terms: Public domain W3C validator