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 18	1 ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   “ cima 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  imaeq12d  6053  nfimad  6065  csbima12  6076  elimasni  6089  inisegn0  6096  csbrn  6203  ressn  6287  csbpredg  6309  predprc  6340  fncofn  6654  foima  6799  focnvimacdmdm  6806  f1imacnv  6839  dffv3  6879  fvco2  6980  sspreima  7065  fimacnvinrn2  7070  rescnvimafod  7071  fsn2  7135  funfvima3  7240  isofrlem  7346  isoselem  7347  fnexALT  7961  mptcnfimad  7996  curry1  8113  curry2  8116  fparlem3  8123  fparlem4  8124  suppsnop  8188  ressuppssdif  8195  suppco  8216  imacosupp  8219  naddcllem  8678  eceq1  8750  uniqs2  8790  ecinxp  8806  mapsnd  8907  sbthlem2  9100  sbth  9109  sbthfi  9207  phplem2  9213  php3  9217  marypha1lem  9418  cantnfp1lem3  9674  tcrank  9894  fin4en1  10380  fin1a2lem7  10477  hsmexlem4  10500  hsmexlem5  10501  fpwwe2cbv  10708  fpwwe2lem3  10711  fpwwe2lem12  10720  fpwwecbv  10722  canth4  10725  f1resfz0f1d  13920  resunimafz0  14583  limsupgval  15636  isercoll  15828  vdwlem1  17152  vdwlem6  17157  vdwlem7  17158  vdwlem8  17159  vdwlem12  17163  vdwlem13  17164  vdwnn  17169  0ram  17191  ramz2  17195  isacs1i  17824  acsficl  18714  gsumvalx  18858  gsumpropd  18860  gsumpropd2lem  18861  gsumress  18864  efgrelexlema  19956  gsumval3a  20110  gsumval3lem1  20112  gsum2dlem2  20178  gsum2d2  20181  dprddisj  20218  dprdf1o  20241  dprdsn  20245  dprd2dlem2  20249  dprd2dlem1  20250  dprd2da  20251  dprd2db  20252  dmdprdsplit2lem  20254  dpjfval  20264  rngqiprngimf1  21589  frlmup3  22099  islindf  22111  islindf2  22113  lindfind  22115  f1lindf  22121  lmimlbs  22135  coe1mul2lem2  22580  subbascn  23565  cncls2  23584  cncls  23585  cnntr  23586  cnpresti  23599  cnprest  23600  cnt1  23661  cnhaus  23665  cncmp  23703  cnconn  23733  1stcfb  23756  xkoccn  23931  ptrescn  23951  xkococnlem  23971  qtopeu  24028  qtoprest  24029  kqdisj  24044  kqcldsat  24045  ordthmeolem  24113  fmfnfmlem4  24269  ustuqtoplem  24551  utopsnneiplem  24559  utopsnneip  24560  ucncn  24596  metustto  24865  metustexhalf  24868  metustfbas  24869  cfilucfil  24871  metuust  24872  cfilucfil2  24873  metuel  24876  metuel2  24877  psmetutop  24879  restmetu  24882  metucn  24883  pi1addval  25362  iscph  25484  cphsscph  25565  uniioombllem3  25899  dyadmbl  25914  mbfima  25944  mbfimaicc  25945  mbfimasn  25946  ismbfd  25953  ismbf2d  25954  ismbf3d  25968  mbfimaopnlem  25969  i1fd  25995  i1f1  26004  itg11  26005  i1faddlem  26007  i1fmullem  26008  i1fadd  26009  itg1addlem3  26012  itg1mulc  26018  itg2gt0  26074  limcnlp  26191  ellimc3  26192  limcflf  26194  limciun  26207  mdegval  26374  mdeg0  26381  mdegvsca  26387  mdegpropd  26395  deg1val  26407  ig1pval  26487  coeeu  26537  coeeq  26539  pserulm  26742  areambl  27279  cutsval  28159  madeval  28211  addbday  28397  negsval  28404  bdayons  28655  zcuts0  28787  bdaypw2n0bndlem  28842  dfpth2  30307  pthhashvtx  30308  pthdlem2  30347  cyclnumvtx  30381  eupth2lem3  30830  eupth2  30833  issh  31803  isch  31817  shsval  31907  2ndimaxp  33233  fnpreimac  33257  dfcnv2  33262  mptiffisupp  33279  indsupp  33427  indfsid  33429  swrdrndisj  33511  pwrssmgc  33554  gsummpt2co  33602  gsumpart  33617  gsumhashmul  33621  cycpmco2rn  33679  qusrn  33953  elrspunidl  33971  rhmimaidl  33975  r1pquslmic  34135  psrbasfsupp  34136  esplyfval  34188  esplyfval0  34189  esplyfval2  34190  vieta  34205  dimval  34226  dimvalfi  34227  ply1degltdimlem  34247  extdgval  34278  algextdeglem3  34344  algextdeglem4  34345  algextdeglem5  34346  smatrcl  34421  locfinreflem  34465  zarclsint  34497  rhmpreimacn  34510  zrhunitpreima  34601  mbfmco2  34890  sibfima  34963  sibfof  34965  eulerpartlemgv  34998  eulerpartlemn  35006  eulerpart  35007  orvcval4  35086  orvcelval  35094  orvcelel  35095  ballotlemscr  35144  fnrelpredd  35709  fineqvr1ombregs  35789  onvfowev  35878  erdszelem3  35937  erdsze  35946  cvmliftlem3  36031  cvmliftlem7  36035  cvmlift2lem9a  36047  msrval  36282  mvtinf  36299  mclsval  36307  mclsax  36313  mthmpps  36326  opelco3  36519  funpartlem  36686  tailval  37141  ptrest  38517  poimirlem1  38519  poimirlem2  38520  poimirlem3  38521  poimirlem4  38522  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem9  38527  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem13  38531  poimirlem14  38532  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem22  38540  poimirlem23  38541  poimirlem24  38542  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  poimirlem28  38546  poimirlem29  38547  poimirlem31  38549  poimirlem32  38550  mblfinlem2  38556  volsupnfl  38563  itg2addnclem2  38570  sstotbnd2  38688  ismtyhmeolem  38718  grpokerinj  38807  lkrfval  40124  aks6d1c6lem5  43207  aks6d1c7lem3  43212  dnnumch3lem  44032  aomclem8  44047  pwfi2f1o  44082  cytpval  44188  frege97d  44737  frege109d  44742  frege131d  44749  nzprmdif  45288  relpfrlem  45921  wessf1ornlem  46169  limsuplesup  46678  limsupvaluz  46687  limsuplt2  46732  limsupge  46740  liminfgval  46741  liminfval2  46747  liminflelimsuplem  46754  liminflelimsup  46755  preimaioomnf  47698  tmachlem-agreefin  47927  tmachlem-franscan  47928  fcoreslem2  48103  f1cof1blem  48113  3f1oss1  48114  afv2co2  48296  imarnf1pr  48321  preimafvelsetpreimafv  48439  imaelsetpreimafv  48446  imasetpreimafvbijlemfo  48456  fundcmpsurbijinjpreimafv  48458  fundcmpsurinj  48460  fundcmpsurbijinj  48461  isgrim  48949  grimuhgr  48954  grimcnv  48955  grimco  48956  uhgrimedgi  48957  isuspgrim0lem  48960  isuspgrim0  48961  upgrimwlklem3  48966  upgrimtrls  48973  upgrimpths  48976  gricushgr  48984  cycldlenngric  48995  isubgrgrim  48996  uhgrimisgrgriclem  48997  clnbgrgrimlem  49000  clnbgrgrim  49001  grimedg  49002  cycl3grtri  49014  isubgr3stgrlem4  49036  uspgrlimlem3  49057  predisj  49890  imasubclem3  50183