Theorem imaeq2d 6064

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by:  imaeq12d  6065  nfimad  6073  csbima12  6083  elimasni  6095  inisegn0  6102  csbrn  6206  ressn  6290  csbpredg  6312  predprc  6343  fncofn  6656  foima  6801  focnvimacdmdm  6808  f1imacnv  6841  dffv3  6881  fvco2  6982  sspreima  7067  fimacnvinrn2  7071  rescnvimafod  7072  fsn2  7136  funfvima3  7238  isofrlem  7344  isoselem  7345  fnexALT  7950  mptcnfimad  7985  curry1  8101  curry2  8104  fparlem3  8111  fparlem4  8112  suppsnop  8176  ressuppssdif  8183  suppco  8204  imacosupp  8207  naddcllem  8664  eceq1  8736  uniqs2  8776  ecinxp  8792  mapsnd  8886  sbthlem2  9079  sbth  9088  sbthfi  9186  phplem2  9192  php3  9196  marypha1lem  9396  cantnfp1lem3  9652  tcrank  9859  fin4en1  10304  fin1a2lem7  10401  hsmexlem4  10424  hsmexlem5  10425  fpwwe2cbv  10626  fpwwe2lem3  10629  fpwwe2lem12  10638  fpwwecbv  10640  canth4  10643  f1resfz0f1d  13834  resunimafz0  14496  limsupgval  15547  isercoll  15739  vdwlem1  17059  vdwlem6  17064  vdwlem7  17065  vdwlem8  17066  vdwlem12  17070  vdwlem13  17071  vdwnn  17076  0ram  17098  ramz2  17102  isacs1i  17731  acsficl  18621  gsumvalx  18756  gsumpropd  18758  gsumpropd2lem  18759  gsumress  18762  efgrelexlema  19843  gsumval3a  19997  gsumval3lem1  19999  gsum2dlem2  20065  gsum2d2  20068  dprddisj  20105  dprdf1o  20128  dprdsn  20132  dprd2dlem2  20136  dprd2dlem1  20137  dprd2da  20138  dprd2db  20139  dmdprdsplit2lem  20141  dpjfval  20151  rngqiprngimf1  21470  frlmup3  21980  islindf  21992  islindf2  21994  lindfind  21996  f1lindf  22002  lmimlbs  22016  coe1mul2lem2  22459  subbascn  23441  cncls2  23460  cncls  23461  cnntr  23462  cnpresti  23475  cnprest  23476  cnt1  23537  cnhaus  23541  cncmp  23579  cnconn  23609  1stcfb  23632  xkoccn  23807  ptrescn  23827  xkococnlem  23847  qtopeu  23904  qtoprest  23905  kqdisj  23920  kqcldsat  23921  ordthmeolem  23989  fmfnfmlem4  24145  ustuqtoplem  24427  utopsnneiplem  24435  utopsnneip  24436  ucncn  24472  metustto  24741  metustexhalf  24744  metustfbas  24745  cfilucfil  24747  metuust  24748  cfilucfil2  24749  metuel  24752  metuel2  24753  psmetutop  24755  restmetu  24758  metucn  24759  pi1addval  25238  iscph  25360  cphsscph  25441  uniioombllem3  25775  dyadmbl  25790  mbfima  25820  mbfimaicc  25821  mbfimasn  25822  ismbfd  25829  ismbf2d  25830  ismbf3d  25844  mbfimaopnlem  25845  i1fd  25871  i1f1  25880  itg11  25881  i1faddlem  25883  i1fmullem  25884  i1fadd  25885  itg1addlem3  25888  itg1mulc  25894  itg2gt0  25950  limcnlp  26068  ellimc3  26069  limcflf  26071  limciun  26084  mdegval  26251  mdeg0  26258  mdegvsca  26264  mdegpropd  26272  deg1val  26284  ig1pval  26364  coeeu  26413  coeeq  26415  pserulm  26616  areambl  27154  cutsval  28004  madeval  28056  addbday  28242  negsval  28249  bdayons  28500  zcuts0  28632  bdaypw2n0bndlem  28687  dfpth2  30117  pthhashvtx  30118  pthdlem2  30157  cyclnumvtx  30191  eupth2lem3  30634  eupth2  30637  issh  31607  isch  31621  shsval  31711  2ndimaxp  33038  fnpreimac  33062  dfcnv2  33067  mptiffisupp  33085  indsupp  33233  indfsid  33235  swrdrndisj  33317  pwrssmgc  33360  gsummpt2co  33408  gsumpart  33423  gsumhashmul  33427  cycpmco2rn  33485  qusrn  33758  elrspunidl  33776  rhmimaidl  33780  r1pquslmic  33940  psrbasfsupp  33941  esplyfval  33993  esplyfval0  33994  esplyfval2  33995  vieta  34010  dimval  34031  dimvalfi  34032  ply1degltdimlem  34052  extdgval  34083  algextdeglem3  34149  algextdeglem4  34150  algextdeglem5  34151  smatrcl  34226  locfinreflem  34270  zarclsint  34302  rhmpreimacn  34315  zrhunitpreima  34406  mbfmco2  34696  sibfima  34769  sibfof  34771  eulerpartlemgv  34804  eulerpartlemn  34812  eulerpart  34813  orvcval4  34892  orvcelval  34900  orvcelel  34901  ballotlemscr  34950  fnrelpredd  35516  fineqvr1ombregs  35584  onvfowev  35633  erdszelem3  35698  erdsze  35707  cvmliftlem3  35792  cvmliftlem7  35796  cvmlift2lem9a  35808  msrval  36043  mvtinf  36060  mclsval  36068  mclsax  36074  mthmpps  36087  opelco3  36280  funpartlem  36447  tailval  36917  ptrest  38303  poimirlem1  38305  poimirlem2  38306  poimirlem3  38307  poimirlem4  38308  poimirlem5  38309  poimirlem6  38310  poimirlem7  38311  poimirlem9  38313  poimirlem10  38314  poimirlem11  38315  poimirlem12  38316  poimirlem13  38317  poimirlem14  38318  poimirlem15  38319  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem22  38326  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  poimirlem28  38332  poimirlem29  38333  poimirlem31  38335  poimirlem32  38336  mblfinlem2  38342  volsupnfl  38349  itg2addnclem2  38356  sstotbnd2  38458  ismtyhmeolem  38488  grpokerinj  38577  lkrfval  39894  aks6d1c6lem5  42977  aks6d1c7lem3  42982  dnnumch3lem  43806  aomclem8  43821  pwfi2f1o  43856  cytpval  43962  frege97d  44511  frege109d  44516  frege131d  44523  nzprmdif  45062  relpfrlem  45695  wessf1ornlem  45936  limsuplesup  46446  limsupvaluz  46455  limsuplt2  46500  limsupge  46508  liminfgval  46509  liminfval2  46515  liminflelimsuplem  46522  liminflelimsup  46523  preimaioomnf  47466  fcoreslem2  47834  f1cof1blem  47844  3f1oss1  47845  afv2co2  48027  imarnf1pr  48052  preimafvelsetpreimafv  48170  imaelsetpreimafv  48177  imasetpreimafvbijlemfo  48187  fundcmpsurbijinjpreimafv  48189  fundcmpsurinj  48191  fundcmpsurbijinj  48192  isgrim  48680  grimuhgr  48685  grimcnv  48686  grimco  48687  uhgrimedgi  48688  isuspgrim0lem  48691  isuspgrim0  48692  upgrimwlklem3  48697  upgrimtrls  48704  upgrimpths  48707  gricushgr  48715  cycldlenngric  48726  isubgrgrim  48727  uhgrimisgrgriclem  48728  clnbgrgrimlem  48731  clnbgrgrim  48732  grimedg  48733  cycl3grtri  48745  isubgr3stgrlem4  48767  uspgrlimlem3  48788  predisj  49622  imasubclem3  49917