Theorem imaeq2d 6025

Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Hypothesis

Ref	Expression
imaeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
imaeq2d	⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Proof of Theorem imaeq2d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		imaeq2 6021	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1542   “ cima 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  imaeq12d  6026  nfimad  6034  csbima12  6044  elimasni  6056  inisegn0  6063  csbrn  6167  ressn  6249  csbpredg  6271  predprc  6302  fncofn  6615  foima  6757  focnvimacdmdm  6764  f1imacnv  6796  dffv3  6836  fvco2  6937  sspreima  7020  fimacnvinrn2  7024  rescnvimafod  7025  fsn2  7089  funfvima3  7191  isofrlem  7295  isoselem  7296  fnexALT  7904  mptcnfimad  7939  curry1  8054  curry2  8057  fparlem3  8064  fparlem4  8065  suppsnop  8128  ressuppssdif  8135  suppco  8156  imacosupp  8159  naddcllem  8612  eceq1  8683  uniqs2  8723  ecinxp  8739  mapsnd  8834  sbthlem2  9026  sbth  9035  sbthfi  9133  phplem2  9139  php3  9143  marypha1lem  9346  cantnfp1lem3  9601  tcrank  9808  fin4en1  10231  fin1a2lem7  10328  hsmexlem4  10351  hsmexlem5  10352  fpwwe2cbv  10553  fpwwe2lem3  10556  fpwwe2lem12  10565  fpwwecbv  10567  canth4  10570  resunimafz0  14407  limsupgval  15438  isercoll  15630  vdwlem1  16952  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  vdwlem12  16963  vdwlem13  16964  vdwnn  16969  0ram  16991  ramz2  16995  isacs1i  17623  acsficl  18513  gsumvalx  18644  gsumpropd  18646  gsumpropd2lem  18647  gsumress  18650  efgrelexlema  19724  gsumval3a  19878  gsumval3lem1  19880  gsum2dlem2  19946  gsum2d2  19949  dprddisj  19986  dprdf1o  20009  dprdsn  20013  dprd2dlem2  20017  dprd2dlem1  20018  dprd2da  20019  dprd2db  20020  dmdprdsplit2lem  20022  dpjfval  20032  rngqiprngimf1  21298  frlmup3  21780  islindf  21792  islindf2  21794  lindfind  21796  f1lindf  21802  lmimlbs  21816  coe1mul2lem2  22233  subbascn  23219  cncls2  23238  cncls  23239  cnntr  23240  cnpresti  23253  cnprest  23254  cnt1  23315  cnhaus  23319  cncmp  23357  cnconn  23387  1stcfb  23410  xkoccn  23584  ptrescn  23604  xkococnlem  23624  qtopeu  23681  qtoprest  23682  kqdisj  23697  kqcldsat  23698  ordthmeolem  23766  fmfnfmlem4  23922  ustuqtoplem  24204  utopsnneiplem  24212  utopsnneip  24213  ucncn  24249  metustto  24518  metustexhalf  24521  metustfbas  24522  cfilucfil  24524  metuust  24525  cfilucfil2  24526  metuel  24529  metuel2  24530  psmetutop  24532  restmetu  24535  metucn  24536  pi1addval  25015  iscph  25137  cphsscph  25218  uniioombllem3  25552  dyadmbl  25567  mbfima  25597  mbfimaicc  25598  mbfimasn  25599  ismbfd  25606  ismbf2d  25607  ismbf3d  25621  mbfimaopnlem  25622  i1fd  25648  i1f1  25657  itg11  25658  i1faddlem  25660  i1fmullem  25661  i1fadd  25662  itg1addlem3  25665  itg1mulc  25671  itg2gt0  25727  limcnlp  25845  ellimc3  25846  limcflf  25848  limciun  25861  mdegval  26028  mdeg0  26035  mdegvsca  26041  mdegpropd  26049  deg1val  26061  ig1pval  26141  coeeu  26190  coeeq  26192  pserulm  26387  areambl  26922  cutsval  27772  madeval  27824  addbday  28010  negsval  28017  bdayons  28268  zcuts0  28400  bdaypw2n0bndlem  28455  dfpth2  29797  pthdlem2  29836  cyclnumvtx  29868  eupth2lem3  30306  eupth2  30309  issh  31279  isch  31293  shsval  31383  2ndimaxp  32719  fnpreimac  32743  dfcnv2  32748  mptiffisupp  32766  indsupp  32927  indfsid  32929  s2rnOLD  33004  s3rnOLD  33006  swrdrndisj  33017  pwrssmgc  33060  gsummpt2co  33109  gsumpart  33124  gsumhashmul  33128  cycpmco2rn  33186  qusrn  33469  elrspunidl  33488  rhmimaidl  33492  r1pquslmic  33671  psrbasfsupp  33672  esplyfval  33707  esplyfval0  33708  esplyfval2  33709  vieta  33724  dimval  33745  dimvalfi  33746  ply1degltdimlem  33766  extdgval  33797  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  smatrcl  33940  locfinreflem  33984  zarclsint  34016  rhmpreimacn  34029  zrhunitpreima  34120  mbfmco2  34409  sibfima  34482  sibfof  34484  eulerpartlemgv  34517  eulerpartlemn  34525  eulerpart  34526  orvcval4  34605  orvcelval  34613  orvcelel  34614  ballotlemscr  34663  fnrelpredd  35234  fineqvr1ombregs  35282  f1resfz0f1d  35296  pthhashvtx  35310  erdszelem3  35375  erdsze  35384  cvmliftlem3  35469  cvmliftlem7  35473  cvmlift2lem9a  35485  msrval  35720  mvtinf  35737  mclsval  35745  mclsax  35751  mthmpps  35764  opelco3  35957  funpartlem  36124  tailval  36555  ptrest  37940  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  poimirlem32  37973  mblfinlem2  37979  volsupnfl  37986  itg2addnclem2  37993  sstotbnd2  38095  ismtyhmeolem  38125  grpokerinj  38214  lkrfval  39533  aks6d1c6lem5  42616  aks6d1c7lem3  42621  dnnumch3lem  43474  aomclem8  43489  pwfi2f1o  43524  cytpval  43630  frege97d  44179  frege109d  44184  frege131d  44191  nzprmdif  44746  relpfrlem  45380  wessf1ornlem  45615  limsuplesup  46127  limsupvaluz  46136  limsuplt2  46181  limsupge  46189  liminfgval  46190  liminfval2  46196  liminflelimsuplem  46203  liminflelimsup  46204  preimaioomnf  47147  fcoreslem2  47512  f1cof1blem  47522  3f1oss1  47523  afv2co2  47705  imarnf1pr  47730  preimafvelsetpreimafv  47848  imaelsetpreimafv  47855  imasetpreimafvbijlemfo  47865  fundcmpsurbijinjpreimafv  47867  fundcmpsurinj  47869  fundcmpsurbijinj  47870  isgrim  48358  grimuhgr  48363  grimcnv  48364  grimco  48365  uhgrimedgi  48366  isuspgrim0lem  48369  isuspgrim0  48370  upgrimwlklem3  48375  upgrimtrls  48382  upgrimpths  48385  gricushgr  48393  cycldlenngric  48404  isubgrgrim  48405  uhgrimisgrgriclem  48406  clnbgrgrimlem  48409  clnbgrgrim  48410  grimedg  48411  cycl3grtri  48423  isubgr3stgrlem4  48445  uspgrlimlem3  48466  predisj  49286  imasubclem3  49581