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

Theorem imaeq2d 5190
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 5186 . 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 1455   "cima 4859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419  df-opab 4478  df-xp 4862  df-cnv 4864  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869
This theorem is referenced by:  imaeq12d  5191  nfimad  5199  csbima12  5207  elimasng  5216  elimasni  5217  inisegn0  5222  csbrn  5320  ressn  5395  foima  5825  f1imacnv  5857  dffv3  5888  fvco2  5968  fsn2  6091  funfvima3  6172  isofrlem  6261  isoselem  6262  fnexALT  6791  curry1  6920  curry2  6923  fparlem3  6930  fparlem4  6931  suppsnop  6960  ressuppssdif  6968  imacosupp  6987  eceq1  7430  uniqs2  7456  ecinxp  7469  mapsn  7544  sbthlem2  7714  sbth  7723  phplem4  7785  php3  7789  marypha1lem  7978  cantnfp1lem3  8216  tcrank  8386  fin4en1  8770  fin1a2lem7  8867  hsmexlem4  8890  hsmexlem5  8891  fpwwe2cbv  9086  fpwwe2lem3  9089  fpwwe2lem13  9098  fpwwecbv  9100  canth4  9103  frnnn0fsupp  10958  limsupgval  13589  isercoll  13786  vdwlem1  14986  vdwlem6  14991  vdwlem7  14992  vdwlem8  14993  vdwlem12  14997  vdwlem13  14998  vdwnn  15003  0ram  15033  ramz2  15037  isacs1i  15618  acsficl  16472  gsumvalx  16568  gsumpropd  16570  gsumpropd2lem  16571  gsumress  16574  efgrelexlema  17454  gsumval3a  17592  gsumval3lem1  17594  gsum2dlem2  17658  gsum2d2  17661  dprddisj  17696  dprdf1o  17720  dprdsn  17724  dprd2dlem2  17728  dprd2dlem1  17729  dprd2da  17730  dprd2db  17731  dmdprdsplit2lem  17733  dpjfval  17743  coe1mul2lem2  18916  frlmup3  19413  islindf  19425  islindf2  19427  lindfind  19429  f1lindf  19435  lmimlbs  19449  subbascn  20325  cncls2  20344  cncls  20345  cnntr  20346  cnpresti  20359  cnprest  20360  cnt1  20421  cnhaus  20425  cncmp  20462  cnconn  20492  1stcfb  20515  xkoccn  20689  ptrescn  20709  xkococnlem  20729  qtopeu  20786  qtoprest  20787  kqdisj  20802  kqcldsat  20803  ordthmeolem  20871  fmfnfmlem4  21027  ustuqtoplem  21309  utopsnneiplem  21317  utopsnneip  21318  ucncn  21355  metustto  21623  metustexhalf  21626  metustfbas  21627  cfilucfil  21629  metuust  21630  cfilucfil2  21631  metuel  21634  metuel2  21635  psmetutop  21637  restmetu  21640  metucn  21641  pi1addval  22134  iscph  22203  uniioombllem3  22599  dyadmbl  22614  mbfima  22644  mbfimaicc  22645  mbfimasn  22646  ismbfd  22652  ismbf2d  22653  ismbf3d  22666  mbfimaopnlem  22667  i1fd  22695  i1f1  22704  itg11  22705  i1faddlem  22707  i1fmullem  22708  i1fadd  22709  itg1addlem3  22712  itg1mulc  22718  itg2gt0  22774  limcnlp  22889  ellimc3  22890  limcflf  22892  limciun  22905  mdegval  23068  mdeg0  23075  mdegvsca  23081  mdegpropd  23089  deg1val  23101  ig1pval  23180  ig1pvalOLD  23186  coeeu  23235  coeeq  23237  pserulm  23433  areambl  23940  spthispth  25359  1pthonlem2  25376  constr2pth  25387  constr3pthlem3  25441  eupath2lem3  25763  eupath2  25764  efghgrpOLD  26157  issh  26917  isch  26931  shsval  27021  fimacnvinrn2  28289  sspreima  28299  dfcnv2  28331  gsummpt2co  28594  smatrcl  28673  locfinreflem  28718  zrhunitpreima  28833  mbfmco2  29137  sibfima  29221  sibfof  29223  eulerpartlemgv  29256  eulerpartlemn  29264  eulerpart  29265  orvcval4  29343  orvcelval  29351  orvcelel  29352  ballotlemscr  29401  ballotlemscrOLD  29439  erdszelem3  29966  erdsze  29975  cvmliftlem3  30060  cvmliftlem7  30064  cvmlift2lem9a  30076  msrval  30226  mvtinf  30243  mclsval  30251  mclsax  30257  mthmpps  30270  opelco3  30470  nofulllem1  30641  nofulllem2  30642  funpartlem  30759  tailval  31079  csbpredg  31773  ptrest  31985  poimirlem1  31987  poimirlem2  31988  poimirlem3  31989  poimirlem4  31990  poimirlem5  31991  poimirlem6  31992  poimirlem7  31993  poimirlem9  31995  poimirlem10  31996  poimirlem11  31997  poimirlem12  31998  poimirlem13  31999  poimirlem14  32000  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem19  32005  poimirlem20  32006  poimirlem22  32008  poimirlem23  32009  poimirlem24  32010  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  poimirlem28  32014  poimirlem29  32015  poimirlem31  32017  poimirlem32  32018  mblfinlem2  32024  volsupnfl  32031  itg2addnclem2  32040  sstotbnd2  32152  ismtyhmeolem  32182  grpokerinj  32229  lkrfval  32699  dnnumch3lem  35950  aomclem8  35965  pwfi2f1o  36000  cytpval  36132  frege97d  36390  frege109d  36395  frege131d  36402  nzprmdif  36713  csbfv12gALTOLD  37254  wessf1ornlem  37513  mapsnd  37530  imarnf1pr  39154  pthdlem2  39890  usgra2pthspth  40034  usgra2adedglem1  40039
  Copyright terms: Public domain W3C validator