Theorem imaeq2d 6052

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is referenced by:  imaeq12d  6053  nfimad  6061  csbima12  6071  elimasni  6083  inisegn0  6090  csbrn  6197  ressn  6279  csbpredg  6301  predprc  6332  fncofn  6660  foima  6800  focnvimacdmdm  6807  f1imacnv  6839  dffv3  6877  fvco2  6981  sspreima  7063  fimacnvinrn2  7067  rescnvimafod  7068  fsn2  7131  funfvima3  7233  isofrlem  7338  isoselem  7339  fnexALT  7954  mptcnfimad  7990  curry1  8108  curry2  8111  fparlem3  8118  fparlem4  8119  suppsnop  8182  ressuppssdif  8189  suppco  8210  imacosupp  8213  naddcllem  8693  eceq1  8763  uniqs2  8798  ecinxp  8811  mapsnd  8905  sbthlem2  9103  sbth  9112  sbthfi  9218  phplem2  9224  php3  9228  php3OLD  9238  marypha1lem  9450  cantnfp1lem3  9699  tcrank  9903  fin4en1  10328  fin1a2lem7  10425  hsmexlem4  10448  hsmexlem5  10449  fpwwe2cbv  10649  fpwwe2lem3  10652  fpwwe2lem12  10661  fpwwecbv  10663  canth4  10666  resunimafz0  14468  limsupgval  15497  isercoll  15689  vdwlem1  17006  vdwlem6  17011  vdwlem7  17012  vdwlem8  17013  vdwlem12  17017  vdwlem13  17018  vdwnn  17023  0ram  17045  ramz2  17049  isacs1i  17674  acsficl  18562  gsumvalx  18659  gsumpropd  18661  gsumpropd2lem  18662  gsumress  18665  efgrelexlema  19735  gsumval3a  19889  gsumval3lem1  19891  gsum2dlem2  19957  gsum2d2  19960  dprddisj  19997  dprdf1o  20020  dprdsn  20024  dprd2dlem2  20028  dprd2dlem1  20029  dprd2da  20030  dprd2db  20031  dmdprdsplit2lem  20033  dpjfval  20043  rngqiprngimf1  21266  frlmup3  21765  islindf  21777  islindf2  21779  lindfind  21781  f1lindf  21787  lmimlbs  21801  coe1mul2lem2  22210  subbascn  23197  cncls2  23216  cncls  23217  cnntr  23218  cnpresti  23231  cnprest  23232  cnt1  23293  cnhaus  23297  cncmp  23335  cnconn  23365  1stcfb  23388  xkoccn  23562  ptrescn  23582  xkococnlem  23602  qtopeu  23659  qtoprest  23660  kqdisj  23675  kqcldsat  23676  ordthmeolem  23744  fmfnfmlem4  23900  ustuqtoplem  24183  utopsnneiplem  24191  utopsnneip  24192  ucncn  24228  metustto  24497  metustexhalf  24500  metustfbas  24501  cfilucfil  24503  metuust  24504  cfilucfil2  24505  metuel  24508  metuel2  24509  psmetutop  24511  restmetu  24514  metucn  24515  pi1addval  25004  iscph  25127  cphsscph  25208  uniioombllem3  25543  dyadmbl  25558  mbfima  25588  mbfimaicc  25589  mbfimasn  25590  ismbfd  25597  ismbf2d  25598  ismbf3d  25612  mbfimaopnlem  25613  i1fd  25639  i1f1  25648  itg11  25649  i1faddlem  25651  i1fmullem  25652  i1fadd  25653  itg1addlem3  25656  itg1mulc  25662  itg2gt0  25718  limcnlp  25836  ellimc3  25837  limcflf  25839  limciun  25852  mdegval  26025  mdeg0  26032  mdegvsca  26038  mdegpropd  26046  deg1val  26058  ig1pval  26138  coeeu  26187  coeeq  26189  pserulm  26388  areambl  26925  scutval  27769  madeval  27817  addsbday  27981  negsval  27988  bdayon  28230  dfpth2  29716  pthdlem2  29755  cyclnumvtx  29787  eupth2lem3  30222  eupth2  30225  issh  31194  isch  31208  shsval  31298  2ndimaxp  32629  fnpreimac  32654  dfcnv2  32659  mptiffisupp  32675  indsupp  32849  s2rnOLD  32924  s3rnOLD  32926  swrdrndisj  32938  pwrssmgc  32985  gsummpt2co  33047  gsumpart  33056  gsumhashmul  33060  cycpmco2rn  33141  qusrn  33429  elrspunidl  33448  rhmimaidl  33452  r1pquslmic  33625  dimval  33645  dimvalfi  33646  ply1degltdimlem  33667  extdgval  33700  algextdeglem3  33758  algextdeglem4  33759  algextdeglem5  33760  smatrcl  33832  locfinreflem  33876  zarclsint  33908  rhmpreimacn  33921  zrhunitpreima  34012  mbfmco2  34302  sibfima  34375  sibfof  34377  eulerpartlemgv  34410  eulerpartlemn  34418  eulerpart  34419  orvcval4  34498  orvcelval  34506  orvcelel  34507  ballotlemscr  34556  fnrelpredd  35125  f1resfz0f1d  35141  pthhashvtx  35155  erdszelem3  35220  erdsze  35229  cvmliftlem3  35314  cvmliftlem7  35318  cvmlift2lem9a  35330  msrval  35565  mvtinf  35582  mclsval  35590  mclsax  35596  mthmpps  35609  opelco3  35797  funpartlem  35965  tailval  36396  ptrest  37648  poimirlem1  37650  poimirlem2  37651  poimirlem3  37652  poimirlem4  37653  poimirlem5  37654  poimirlem6  37655  poimirlem7  37656  poimirlem9  37658  poimirlem10  37659  poimirlem11  37660  poimirlem12  37661  poimirlem13  37662  poimirlem14  37663  poimirlem15  37664  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem22  37671  poimirlem23  37672  poimirlem24  37673  poimirlem25  37674  poimirlem26  37675  poimirlem27  37676  poimirlem28  37677  poimirlem29  37678  poimirlem31  37680  poimirlem32  37681  mblfinlem2  37687  volsupnfl  37694  itg2addnclem2  37701  sstotbnd2  37803  ismtyhmeolem  37833  grpokerinj  37922  lkrfval  39110  aks6d1c6lem5  42195  aks6d1c7lem3  42200  dnnumch3lem  43045  aomclem8  43060  pwfi2f1o  43095  cytpval  43201  frege97d  43751  frege109d  43756  frege131d  43763  nzprmdif  44318  relpfrlem  44953  wessf1ornlem  45189  limsuplesup  45708  limsupvaluz  45717  limsuplt2  45762  limsupge  45770  liminfgval  45771  liminfval2  45777  liminflelimsuplem  45784  liminflelimsup  45785  preimaioomnf  46728  fcoreslem2  47073  f1cof1blem  47083  3f1oss1  47084  afv2co2  47266  imarnf1pr  47291  preimafvelsetpreimafv  47382  imaelsetpreimafv  47389  imasetpreimafvbijlemfo  47399  fundcmpsurbijinjpreimafv  47401  fundcmpsurinj  47403  fundcmpsurbijinj  47404  isgrim  47875  grimuhgr  47880  grimcnv  47881  grimco  47882  uhgrimedgi  47883  isuspgrim0lem  47886  isuspgrim0  47887  upgrimwlklem3  47892  upgrimtrls  47899  upgrimpths  47902  gricushgr  47910  cycldlenngric  47921  isubgrgrim  47922  uhgrimisgrgriclem  47923  clnbgrgrimlem  47926  clnbgrgrim  47927  grimedg  47928  cycl3grtri  47939  isubgr3stgrlem4  47961  uspgrlimlem3  47982  predisj  48769  imasubclem3  49045