Theorem imaeq2d 5986

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5087  df-opab 5149  df-xp 5613  df-cnv 5615  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620

This theorem is referenced by:  imaeq12d  5987  nfimad  5995  csbima12  6004  elimasngOLD  6015  elimasni  6016  inisegn0  6023  csbrn  6128  ressn  6210  csbpredg  6230  predprc  6263  fncofn  6586  foima  6730  focnvimacdmdm  6737  f1imacnv  6769  dffv3  6807  fvco2  6904  sspreima  6984  fimacnvinrn2  6989  rescnvimafod  6990  fsn2  7047  funfvima3  7151  isofrlem  7250  isoselem  7251  fnexALT  7839  curry1  7990  curry2  7993  fparlem3  8000  fparlem4  8001  suppsnop  8042  ressuppssdif  8049  suppco  8070  imacosupp  8073  eceq1  8585  uniqs2  8617  ecinxp  8630  mapsnd  8723  sbthlem2  8927  sbth  8936  sbthfi  9045  phplem2  9051  php3  9055  phplem4OLD  9063  php3OLD  9067  marypha1lem  9268  cantnfp1lem3  9515  tcrank  9719  fin4en1  10144  fin1a2lem7  10241  hsmexlem4  10264  hsmexlem5  10265  fpwwe2cbv  10465  fpwwe2lem3  10468  fpwwe2lem12  10477  fpwwecbv  10479  canth4  10482  resunimafz0  14235  limsupgval  15261  isercoll  15455  vdwlem1  16756  vdwlem6  16761  vdwlem7  16762  vdwlem8  16763  vdwlem12  16767  vdwlem13  16768  vdwnn  16773  0ram  16795  ramz2  16799  isacs1i  17440  acsficl  18339  gsumvalx  18434  gsumpropd  18436  gsumpropd2lem  18437  gsumress  18440  efgrelexlema  19427  gsumval3a  19576  gsumval3lem1  19578  gsum2dlem2  19644  gsum2d2  19647  dprddisj  19684  dprdf1o  19707  dprdsn  19711  dprd2dlem2  19715  dprd2dlem1  19716  dprd2da  19717  dprd2db  19718  dmdprdsplit2lem  19720  dpjfval  19730  frlmup3  21087  islindf  21099  islindf2  21101  lindfind  21103  f1lindf  21109  lmimlbs  21123  coe1mul2lem2  21519  subbascn  22485  cncls2  22504  cncls  22505  cnntr  22506  cnpresti  22519  cnprest  22520  cnt1  22581  cnhaus  22585  cncmp  22623  cnconn  22653  1stcfb  22676  xkoccn  22850  ptrescn  22870  xkococnlem  22890  qtopeu  22947  qtoprest  22948  kqdisj  22963  kqcldsat  22964  ordthmeolem  23032  fmfnfmlem4  23188  ustuqtoplem  23471  utopsnneiplem  23479  utopsnneip  23480  ucncn  23517  metustto  23789  metustexhalf  23792  metustfbas  23793  cfilucfil  23795  metuust  23796  cfilucfil2  23797  metuel  23800  metuel2  23801  psmetutop  23803  restmetu  23806  metucn  23807  pi1addval  24291  iscph  24414  cphsscph  24495  uniioombllem3  24829  dyadmbl  24844  mbfima  24874  mbfimaicc  24875  mbfimasn  24876  ismbfd  24883  ismbf2d  24884  ismbf3d  24898  mbfimaopnlem  24899  i1fd  24925  i1f1  24934  itg11  24935  i1faddlem  24937  i1fmullem  24938  i1fadd  24939  itg1addlem3  24942  itg1mulc  24949  itg2gt0  25005  limcnlp  25122  ellimc3  25123  limcflf  25125  limciun  25138  mdegval  25308  mdeg0  25315  mdegvsca  25321  mdegpropd  25329  deg1val  25341  ig1pval  25417  coeeu  25466  coeeq  25468  pserulm  25661  areambl  26188  pthdlem2  28268  eupth2lem3  28732  eupth2  28735  issh  29702  isch  29716  shsval  29806  2ndimaxp  31115  fnpreimac  31139  dfcnv2  31144  s2rn  31349  s3rn  31351  swrdrndisj  31360  pwrssmgc  31409  gsummpt2co  31439  gsumpart  31446  gsumhashmul  31447  cycpmco2rn  31523  elrspunidl  31741  rhmimaidl  31744  dimval  31822  dimvalfi  31823  extdgval  31865  smatrcl  31882  locfinreflem  31926  zarclsint  31958  rhmpreimacn  31971  zrhunitpreima  32064  mbfmco2  32368  sibfima  32441  sibfof  32443  eulerpartlemgv  32476  eulerpartlemn  32484  eulerpart  32485  orvcval4  32563  orvcelval  32571  orvcelel  32572  ballotlemscr  32621  fnrelpredd  33196  f1resfz0f1d  33207  pthhashvtx  33224  erdszelem3  33290  erdsze  33299  cvmliftlem3  33384  cvmliftlem7  33388  cvmlift2lem9a  33400  msrval  33635  mvtinf  33652  mclsval  33660  mclsax  33666  mthmpps  33679  opelco3  33876  naddcllem  33954  scutval  34064  madeval  34106  negsval  34193  funpartlem  34314  tailval  34632  ptrest  35853  poimirlem1  35855  poimirlem2  35856  poimirlem3  35857  poimirlem4  35858  poimirlem5  35859  poimirlem6  35860  poimirlem7  35861  poimirlem9  35863  poimirlem10  35864  poimirlem11  35865  poimirlem12  35866  poimirlem13  35867  poimirlem14  35868  poimirlem15  35869  poimirlem16  35870  poimirlem17  35871  poimirlem19  35873  poimirlem20  35874  poimirlem22  35876  poimirlem23  35877  poimirlem24  35878  poimirlem25  35879  poimirlem26  35880  poimirlem27  35881  poimirlem28  35882  poimirlem29  35883  poimirlem31  35885  poimirlem32  35886  mblfinlem2  35892  volsupnfl  35899  itg2addnclem2  35906  sstotbnd2  36009  ismtyhmeolem  36039  grpokerinj  36128  lkrfval  37326  dnnumch3lem  41093  aomclem8  41108  pwfi2f1o  41143  cytpval  41256  frege97d  41599  frege109d  41604  frege131d  41611  nzprmdif  42176  wessf1ornlem  42968  limsuplesup  43495  limsupvaluz  43504  limsuplt2  43549  limsupge  43557  liminfgval  43558  liminfval2  43564  liminflelimsuplem  43571  liminflelimsup  43572  preimaioomnf  44513  fcoreslem2  44828  f1cof1blem  44838  afv2co2  45019  imarnf1pr  45044  preimafvelsetpreimafv  45110  imaelsetpreimafv  45117  imasetpreimafvbijlemfo  45127  fundcmpsurbijinjpreimafv  45129  fundcmpsurinj  45131  fundcmpsurbijinj  45132  isomgr  45545  isomushgr  45548  isomgrsym  45558  isomgrtrlem  45560  predisj  46426