Theorem imaeq2d 6051

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  imaeq12d  6052  nfimad  6064  csbima12  6075  elimasni  6088  inisegn0  6095  csbrn  6204  ressn  6288  csbpredg  6310  predprc  6341  fncofn  6657  foima  6802  focnvimacdmdm  6809  f1imacnv  6842  dffv3  6882  fvco2  6983  sspreima  7068  fimacnvinrn2  7073  rescnvimafod  7074  fsn2  7138  funfvima3  7243  isofrlem  7349  isoselem  7350  fnexALT  7964  mptcnfimad  7999  curry1  8118  curry2  8121  fparlem3  8128  fparlem4  8129  suppsnop  8199  ressuppssdif  8206  suppco  8227  imacosupp  8230  naddcllem  8689  eceq1  8761  uniqs2  8801  ecinxp  8817  mapsnd  8918  sbthlem2  9111  sbth  9120  sbthfi  9218  phplem2  9224  php3  9228  marypha1lem  9429  cantnfp1lem3  9685  tcrank  9905  fin4en1  10391  fin1a2lem7  10488  hsmexlem4  10511  hsmexlem5  10512  fpwwe2cbv  10719  fpwwe2lem3  10722  fpwwe2lem12  10731  fpwwecbv  10733  canth4  10736  f1resfz0f1d  13931  resunimafz0  14594  limsupgval  15649  isercoll  15841  vdwlem1  17165  vdwlem6  17170  vdwlem7  17171  vdwlem8  17172  vdwlem12  17176  vdwlem13  17177  vdwnn  17182  0ram  17204  ramz2  17208  isacs1i  17837  acsficl  18727  gsumvalx  18871  gsumpropd  18873  gsumpropd2lem  18874  gsumress  18877  efgrelexlema  19969  gsumval3a  20123  gsumval3lem1  20125  gsum2dlem2  20191  gsum2d2  20194  dprddisj  20231  dprdf1o  20254  dprdsn  20258  dprd2dlem2  20262  dprd2dlem1  20263  dprd2da  20264  dprd2db  20265  dmdprdsplit2lem  20267  dpjfval  20277  rngqiprngimf1  21602  frlmup3  22112  islindf  22124  islindf2  22126  lindfind  22128  f1lindf  22134  lmimlbs  22148  coe1mul2lem2  22593  subbascn  23578  cncls2  23597  cncls  23598  cnntr  23599  cnpresti  23612  cnprest  23613  cnt1  23674  cnhaus  23678  cncmp  23716  cnconn  23746  1stcfb  23769  xkoccn  23944  ptrescn  23964  xkococnlem  23984  qtopeu  24041  qtoprest  24042  kqdisj  24057  kqcldsat  24058  ordthmeolem  24126  fmfnfmlem4  24282  ustuqtoplem  24564  utopsnneiplem  24572  utopsnneip  24573  ucncn  24609  metustto  24878  metustexhalf  24881  metustfbas  24882  cfilucfil  24884  metuust  24885  cfilucfil2  24886  metuel  24889  metuel2  24890  psmetutop  24892  restmetu  24895  metucn  24896  pi1addval  25375  iscph  25497  cphsscph  25578  uniioombllem3  25912  dyadmbl  25927  mbfima  25957  mbfimaicc  25958  mbfimasn  25959  ismbfd  25966  ismbf2d  25967  ismbf3d  25981  mbfimaopnlem  25982  i1fd  26008  i1f1  26017  itg11  26018  i1faddlem  26020  i1fmullem  26021  i1fadd  26022  itg1addlem3  26025  itg1mulc  26031  itg2gt0  26087  limcnlp  26204  ellimc3  26205  limcflf  26207  limciun  26220  mdegval  26387  mdeg0  26394  mdegvsca  26400  mdegpropd  26408  deg1val  26420  ig1pval  26500  coeeu  26550  coeeq  26552  pserulm  26755  areambl  27292  cutsval  28172  madeval  28224  addbday  28410  negsval  28417  bdayons  28668  zcuts0  28800  bdaypw2n0bndlem  28855  dfpth2  30320  pthhashvtx  30321  pthdlem2  30360  cyclnumvtx  30394  eupth2lem3  30843  eupth2  30846  issh  31816  isch  31830  shsval  31920  2ndimaxp  33288  fnpreimac  33312  dfcnv2  33317  mptiffisupp  33334  indsupp  33481  indfsid  33483  swrdrndisj  33565  pwrssmgc  33608  gsummpt2co  33656  gsumpart  33671  gsumhashmul  33675  cycpmco2rn  33733  qusrn  34007  elrspunidl  34025  rhmimaidl  34029  r1pquslmic  34189  psrbasfsupp  34190  esplyfval  34242  esplyfval0  34243  esplyfval2  34244  vieta  34259  dimval  34280  dimvalfi  34281  ply1degltdimlem  34301  extdgval  34332  algextdeglem3  34398  algextdeglem4  34399  algextdeglem5  34400  smatrcl  34475  locfinreflem  34519  zarclsint  34551  rhmpreimacn  34564  zrhunitpreima  34655  mbfmco2  34944  sibfima  35017  sibfof  35019  eulerpartlemgv  35052  eulerpartlemn  35060  eulerpart  35061  orvcval4  35140  orvcelval  35148  orvcelel  35149  ballotlemscr  35198  fnrelpredd  35773  fineqvr1ombregs  35863  onvfowev  35970  erdszelem3  36045  erdsze  36054  cvmliftlem3  36139  cvmliftlem7  36143  cvmlift2lem9a  36155  msrval  36390  mvtinf  36407  mclsval  36415  mclsax  36421  mthmpps  36434  opelco3  36632  funpartlem  36799  tailval  37254  ptrest  38631  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem5  38637  poimirlem6  38638  poimirlem7  38639  poimirlem9  38641  poimirlem10  38642  poimirlem11  38643  poimirlem12  38644  poimirlem13  38645  poimirlem14  38646  poimirlem15  38647  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem26  38658  poimirlem27  38659  poimirlem28  38660  poimirlem29  38661  poimirlem31  38663  poimirlem32  38664  mblfinlem2  38670  volsupnfl  38677  itg2addnclem2  38684  sstotbnd2  38802  ismtyhmeolem  38832  grpokerinj  38921  lkrfval  40238  aks6d1c6lem5  43321  aks6d1c7lem3  43326  dnnumch3lem  44147  aomclem8  44157  pwfi2f1o  44192  cytpval  44298  frege97d  44846  frege109d  44851  frege131d  44858  nzprmdif  45397  relpfrlem  46037  wessf1ornlem  46294  limsuplesup  46803  limsupvaluz  46812  limsuplt2  46857  limsupge  46865  liminfgval  46866  liminfval2  46872  liminflelimsuplem  46879  liminflelimsup  46880  preimaioomnf  47823  tmachlem-agreefin  48052  tmachlem-franscan  48053  fcoreslem2  48228  f1cof1blem  48238  3f1oss1  48239  afv2co2  48421  imarnf1pr  48446  preimafvelsetpreimafv  48564  imaelsetpreimafv  48571  imasetpreimafvbijlemfo  48581  fundcmpsurbijinjpreimafv  48583  fundcmpsurinj  48585  fundcmpsurbijinj  48586  isgrim  49074  grimuhgr  49079  grimcnv  49080  grimco  49081  uhgrimedgi  49082  isuspgrim0lem  49085  isuspgrim0  49086  upgrimwlklem3  49091  upgrimtrls  49098  upgrimpths  49101  gricushgr  49109  cycldlenngric  49120  isubgrgrim  49121  uhgrimisgrgriclem  49122  clnbgrgrimlem  49125  clnbgrgrim  49126  grimedg  49127  cycl3grtri  49139  isubgr3stgrlem4  49161  uspgrlimlem3  49182  predisj  50015  imasubclem3  50316