Theorem imaeq2d 6064

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 6060	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1570   “ cima 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is referenced by:  imaeq12d  6065  nfimad  6073  csbima12  6083  elimasni  6095  inisegn0  6102  csbrn  6206  ressn  6288  csbpredg  6310  predprc  6341  fncofn  6654  foima  6799  focnvimacdmdm  6806  f1imacnv  6839  dffv3  6879  fvco2  6980  sspreima  7065  fimacnvinrn2  7069  rescnvimafod  7070  fsn2  7134  funfvima3  7236  isofrlem  7340  isoselem  7341  fnexALT  7949  mptcnfimad  7984  curry1  8100  curry2  8103  fparlem3  8110  fparlem4  8111  suppsnop  8175  ressuppssdif  8182  suppco  8203  imacosupp  8206  naddcllem  8663  eceq1  8735  uniqs2  8775  ecinxp  8791  mapsnd  8885  sbthlem2  9077  sbth  9086  sbthfi  9184  phplem2  9190  php3  9194  marypha1lem  9394  cantnfp1lem3  9650  tcrank  9857  fin4en1  10294  fin1a2lem7  10391  hsmexlem4  10414  hsmexlem5  10415  fpwwe2cbv  10616  fpwwe2lem3  10619  fpwwe2lem12  10628  fpwwecbv  10630  canth4  10633  resunimafz0  14484  limsupgval  15529  isercoll  15721  vdwlem1  17042  vdwlem6  17047  vdwlem7  17048  vdwlem8  17049  vdwlem12  17053  vdwlem13  17054  vdwnn  17059  0ram  17081  ramz2  17085  isacs1i  17714  acsficl  18604  gsumvalx  18735  gsumpropd  18737  gsumpropd2lem  18738  gsumress  18741  efgrelexlema  19820  gsumval3a  19974  gsumval3lem1  19976  gsum2dlem2  20042  gsum2d2  20045  dprddisj  20082  dprdf1o  20105  dprdsn  20109  dprd2dlem2  20113  dprd2dlem1  20114  dprd2da  20115  dprd2db  20116  dmdprdsplit2lem  20118  dpjfval  20128  rngqiprngimf1  21421  frlmup3  21931  islindf  21943  islindf2  21945  lindfind  21947  f1lindf  21953  lmimlbs  21967  coe1mul2lem2  22410  subbascn  23392  cncls2  23411  cncls  23412  cnntr  23413  cnpresti  23426  cnprest  23427  cnt1  23488  cnhaus  23492  cncmp  23530  cnconn  23560  1stcfb  23583  xkoccn  23757  ptrescn  23777  xkococnlem  23797  qtopeu  23854  qtoprest  23855  kqdisj  23870  kqcldsat  23871  ordthmeolem  23939  fmfnfmlem4  24095  ustuqtoplem  24377  utopsnneiplem  24385  utopsnneip  24386  ucncn  24422  metustto  24691  metustexhalf  24694  metustfbas  24695  cfilucfil  24697  metuust  24698  cfilucfil2  24699  metuel  24702  metuel2  24703  psmetutop  24705  restmetu  24708  metucn  24709  pi1addval  25188  iscph  25310  cphsscph  25391  uniioombllem3  25725  dyadmbl  25740  mbfima  25770  mbfimaicc  25771  mbfimasn  25772  ismbfd  25779  ismbf2d  25780  ismbf3d  25794  mbfimaopnlem  25795  i1fd  25821  i1f1  25830  itg11  25831  i1faddlem  25833  i1fmullem  25834  i1fadd  25835  itg1addlem3  25838  itg1mulc  25844  itg2gt0  25900  limcnlp  26018  ellimc3  26019  limcflf  26021  limciun  26034  mdegval  26201  mdeg0  26208  mdegvsca  26214  mdegpropd  26222  deg1val  26234  ig1pval  26314  coeeu  26363  coeeq  26365  pserulm  26566  areambl  27104  cutsval  27954  madeval  28006  addbday  28192  negsval  28199  bdayons  28450  zcuts0  28582  bdaypw2n0bndlem  28637  dfpth2  30059  pthdlem2  30098  cyclnumvtx  30130  eupth2lem3  30568  eupth2  30571  issh  31541  isch  31555  shsval  31645  2ndimaxp  32972  fnpreimac  32996  dfcnv2  33001  mptiffisupp  33019  indsupp  33168  indfsid  33170  s2rnOLD  33245  s3rnOLD  33247  swrdrndisj  33258  pwrssmgc  33301  gsummpt2co  33349  gsumpart  33364  gsumhashmul  33368  cycpmco2rn  33426  qusrn  33699  elrspunidl  33717  rhmimaidl  33721  r1pquslmic  33881  psrbasfsupp  33882  esplyfval  33934  esplyfval0  33935  esplyfval2  33936  vieta  33951  dimval  33972  dimvalfi  33973  ply1degltdimlem  33993  extdgval  34024  algextdeglem3  34090  algextdeglem4  34091  algextdeglem5  34092  smatrcl  34167  locfinreflem  34211  zarclsint  34243  rhmpreimacn  34256  zrhunitpreima  34347  mbfmco2  34636  sibfima  34709  sibfof  34711  eulerpartlemgv  34744  eulerpartlemn  34752  eulerpart  34753  orvcval4  34832  orvcelval  34840  orvcelel  34841  ballotlemscr  34890  fnrelpredd  35463  fineqvr1ombregs  35532  onvfowev  35581  f1resfz0f1d  35586  pthhashvtx  35601  erdszelem3  35666  erdsze  35675  cvmliftlem3  35760  cvmliftlem7  35764  cvmlift2lem9a  35776  msrval  36011  mvtinf  36028  mclsval  36036  mclsax  36042  mthmpps  36055  opelco3  36248  funpartlem  36415  tailval  36865  ptrest  38251  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem9  38261  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem13  38265  poimirlem14  38266  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem22  38274  poimirlem23  38275  poimirlem24  38276  poimirlem25  38277  poimirlem26  38278  poimirlem27  38279  poimirlem28  38280  poimirlem29  38281  poimirlem31  38283  poimirlem32  38284  mblfinlem2  38290  volsupnfl  38297  itg2addnclem2  38304  sstotbnd2  38406  ismtyhmeolem  38436  grpokerinj  38525  lkrfval  39842  aks6d1c6lem5  42925  aks6d1c7lem3  42930  dnnumch3lem  43756  aomclem8  43771  pwfi2f1o  43806  cytpval  43912  frege97d  44461  frege109d  44466  frege131d  44473  nzprmdif  45012  relpfrlem  45645  wessf1ornlem  45886  limsuplesup  46396  limsupvaluz  46405  limsuplt2  46450  limsupge  46458  liminfgval  46459  liminfval2  46465  liminflelimsuplem  46472  liminflelimsup  46473  preimaioomnf  47416  fcoreslem2  47784  f1cof1blem  47794  3f1oss1  47795  afv2co2  47977  imarnf1pr  48002  preimafvelsetpreimafv  48120  imaelsetpreimafv  48127  imasetpreimafvbijlemfo  48137  fundcmpsurbijinjpreimafv  48139  fundcmpsurinj  48141  fundcmpsurbijinj  48142  isgrim  48630  grimuhgr  48635  grimcnv  48636  grimco  48637  uhgrimedgi  48638  isuspgrim0lem  48641  isuspgrim0  48642  upgrimwlklem3  48647  upgrimtrls  48654  upgrimpths  48657  gricushgr  48665  cycldlenngric  48676  isubgrgrim  48677  uhgrimisgrgriclem  48678  clnbgrgrimlem  48681  clnbgrgrim  48682  grimedg  48683  cycl3grtri  48695  isubgr3stgrlem4  48717  uspgrlimlem3  48738  predisj  49572  imasubclem3  49867