Theorem imaeq2d 6020

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  imaeq12d  6021  nfimad  6029  csbima12  6039  elimasni  6051  inisegn0  6058  csbrn  6164  ressn  6246  csbpredg  6268  predprc  6299  fncofn  6617  foima  6759  focnvimacdmdm  6766  f1imacnv  6798  dffv3  6836  fvco2  6940  sspreima  7022  fimacnvinrn2  7026  rescnvimafod  7027  fsn2  7090  funfvima3  7192  isofrlem  7297  isoselem  7298  fnexALT  7909  mptcnfimad  7944  curry1  8060  curry2  8063  fparlem3  8070  fparlem4  8071  suppsnop  8134  ressuppssdif  8141  suppco  8162  imacosupp  8165  naddcllem  8617  eceq1  8687  uniqs2  8727  ecinxp  8742  mapsnd  8836  sbthlem2  9029  sbth  9038  sbthfi  9140  phplem2  9146  php3  9150  marypha1lem  9360  cantnfp1lem3  9609  tcrank  9813  fin4en1  10238  fin1a2lem7  10335  hsmexlem4  10358  hsmexlem5  10359  fpwwe2cbv  10559  fpwwe2lem3  10562  fpwwe2lem12  10571  fpwwecbv  10573  canth4  10576  resunimafz0  14386  limsupgval  15418  isercoll  15610  vdwlem1  16928  vdwlem6  16933  vdwlem7  16934  vdwlem8  16935  vdwlem12  16939  vdwlem13  16940  vdwnn  16945  0ram  16967  ramz2  16971  isacs1i  17594  acsficl  18482  gsumvalx  18579  gsumpropd  18581  gsumpropd2lem  18582  gsumress  18585  efgrelexlema  19655  gsumval3a  19809  gsumval3lem1  19811  gsum2dlem2  19877  gsum2d2  19880  dprddisj  19917  dprdf1o  19940  dprdsn  19944  dprd2dlem2  19948  dprd2dlem1  19949  dprd2da  19950  dprd2db  19951  dmdprdsplit2lem  19953  dpjfval  19963  rngqiprngimf1  21186  frlmup3  21685  islindf  21697  islindf2  21699  lindfind  21701  f1lindf  21707  lmimlbs  21721  coe1mul2lem2  22130  subbascn  23117  cncls2  23136  cncls  23137  cnntr  23138  cnpresti  23151  cnprest  23152  cnt1  23213  cnhaus  23217  cncmp  23255  cnconn  23285  1stcfb  23308  xkoccn  23482  ptrescn  23502  xkococnlem  23522  qtopeu  23579  qtoprest  23580  kqdisj  23595  kqcldsat  23596  ordthmeolem  23664  fmfnfmlem4  23820  ustuqtoplem  24103  utopsnneiplem  24111  utopsnneip  24112  ucncn  24148  metustto  24417  metustexhalf  24420  metustfbas  24421  cfilucfil  24423  metuust  24424  cfilucfil2  24425  metuel  24428  metuel2  24429  psmetutop  24431  restmetu  24434  metucn  24435  pi1addval  24924  iscph  25046  cphsscph  25127  uniioombllem3  25462  dyadmbl  25477  mbfima  25507  mbfimaicc  25508  mbfimasn  25509  ismbfd  25516  ismbf2d  25517  ismbf3d  25531  mbfimaopnlem  25532  i1fd  25558  i1f1  25567  itg11  25568  i1faddlem  25570  i1fmullem  25571  i1fadd  25572  itg1addlem3  25575  itg1mulc  25581  itg2gt0  25637  limcnlp  25755  ellimc3  25756  limcflf  25758  limciun  25771  mdegval  25944  mdeg0  25951  mdegvsca  25957  mdegpropd  25965  deg1val  25977  ig1pval  26057  coeeu  26106  coeeq  26108  pserulm  26307  areambl  26844  scutval  27688  madeval  27736  addsbday  27900  negsval  27907  bdayon  28149  dfpth2  29632  pthdlem2  29671  cyclnumvtx  29703  eupth2lem3  30138  eupth2  30141  issh  31110  isch  31124  shsval  31214  2ndimaxp  32543  fnpreimac  32568  dfcnv2  32573  mptiffisupp  32589  indsupp  32763  s2rnOLD  32838  s3rnOLD  32840  swrdrndisj  32852  pwrssmgc  32899  gsummpt2co  32961  gsumpart  32970  gsumhashmul  32974  cycpmco2rn  33055  qusrn  33353  elrspunidl  33372  rhmimaidl  33376  r1pquslmic  33549  dimval  33569  dimvalfi  33570  ply1degltdimlem  33591  extdgval  33622  algextdeglem3  33682  algextdeglem4  33683  algextdeglem5  33684  smatrcl  33759  locfinreflem  33803  zarclsint  33835  rhmpreimacn  33848  zrhunitpreima  33939  mbfmco2  34229  sibfima  34302  sibfof  34304  eulerpartlemgv  34337  eulerpartlemn  34345  eulerpart  34346  orvcval4  34425  orvcelval  34433  orvcelel  34434  ballotlemscr  34483  fnrelpredd  35052  f1resfz0f1d  35074  pthhashvtx  35088  erdszelem3  35153  erdsze  35162  cvmliftlem3  35247  cvmliftlem7  35251  cvmlift2lem9a  35263  msrval  35498  mvtinf  35515  mclsval  35523  mclsax  35529  mthmpps  35542  opelco3  35735  funpartlem  35903  tailval  36334  ptrest  37586  poimirlem1  37588  poimirlem2  37589  poimirlem3  37590  poimirlem4  37591  poimirlem5  37592  poimirlem6  37593  poimirlem7  37594  poimirlem9  37596  poimirlem10  37597  poimirlem11  37598  poimirlem12  37599  poimirlem13  37600  poimirlem14  37601  poimirlem15  37602  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem22  37609  poimirlem23  37610  poimirlem24  37611  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem28  37615  poimirlem29  37616  poimirlem31  37618  poimirlem32  37619  mblfinlem2  37625  volsupnfl  37632  itg2addnclem2  37639  sstotbnd2  37741  ismtyhmeolem  37771  grpokerinj  37860  lkrfval  39053  aks6d1c6lem5  42138  aks6d1c7lem3  42143  dnnumch3lem  43008  aomclem8  43023  pwfi2f1o  43058  cytpval  43164  frege97d  43714  frege109d  43719  frege131d  43726  nzprmdif  44281  relpfrlem  44916  wessf1ornlem  45152  limsuplesup  45670  limsupvaluz  45679  limsuplt2  45724  limsupge  45732  liminfgval  45733  liminfval2  45739  liminflelimsuplem  45746  liminflelimsup  45747  preimaioomnf  46690  fcoreslem2  47038  f1cof1blem  47048  3f1oss1  47049  afv2co2  47231  imarnf1pr  47256  preimafvelsetpreimafv  47362  imaelsetpreimafv  47369  imasetpreimafvbijlemfo  47379  fundcmpsurbijinjpreimafv  47381  fundcmpsurinj  47383  fundcmpsurbijinj  47384  isgrim  47855  grimuhgr  47860  grimcnv  47861  grimco  47862  uhgrimedgi  47863  isuspgrim0lem  47866  isuspgrim0  47867  upgrimwlklem3  47872  upgrimtrls  47879  upgrimpths  47882  gricushgr  47890  cycldlenngric  47901  isubgrgrim  47902  uhgrimisgrgriclem  47903  clnbgrgrimlem  47906  clnbgrgrim  47907  grimedg  47908  cycl3grtri  47919  isubgr3stgrlem4  47941  uspgrlimlem3  47962  predisj  48772  imasubclem3  49068