Theorem imaeq2d 5972

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

Syntax hints:   → wi 4   = wceq 1539   “ cima 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596  df-cnv 5598  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603

This theorem is referenced by:  imaeq12d  5973  nfimad  5981  csbima12  5990  elimasngOLD  6001  elimasni  6002  inisegn0  6009  csbrn  6111  ressn  6192  csbpredg  6212  predprc  6245  fncofn  6557  foima  6702  focnvimacdmdm  6709  f1imacnv  6741  dffv3  6779  fvco2  6874  sspreima  6954  fimacnvinrn2  6959  rescnvimafod  6960  fsn2  7017  funfvima3  7121  isofrlem  7220  isoselem  7221  fnexALT  7802  curry1  7953  curry2  7956  fparlem3  7963  fparlem4  7964  suppsnop  8003  ressuppssdif  8010  suppco  8031  imacosupp  8034  eceq1  8545  uniqs2  8577  ecinxp  8590  mapsnd  8683  sbthlem2  8880  sbth  8889  sbthfi  8994  phplem2  9000  php3  9004  phplem4OLD  9012  php3OLD  9016  marypha1lem  9201  cantnfp1lem3  9447  tcrank  9651  fin4en1  10074  fin1a2lem7  10171  hsmexlem4  10194  hsmexlem5  10195  fpwwe2cbv  10395  fpwwe2lem3  10398  fpwwe2lem12  10407  fpwwecbv  10409  canth4  10412  resunimafz0  14166  limsupgval  15194  isercoll  15388  vdwlem1  16691  vdwlem6  16696  vdwlem7  16697  vdwlem8  16698  vdwlem12  16702  vdwlem13  16703  vdwnn  16708  0ram  16730  ramz2  16734  isacs1i  17375  acsficl  18274  gsumvalx  18369  gsumpropd  18371  gsumpropd2lem  18372  gsumress  18375  efgrelexlema  19364  gsumval3a  19513  gsumval3lem1  19515  gsum2dlem2  19581  gsum2d2  19584  dprddisj  19621  dprdf1o  19644  dprdsn  19648  dprd2dlem2  19652  dprd2dlem1  19653  dprd2da  19654  dprd2db  19655  dmdprdsplit2lem  19657  dpjfval  19667  frlmup3  21016  islindf  21028  islindf2  21030  lindfind  21032  f1lindf  21038  lmimlbs  21052  coe1mul2lem2  21448  subbascn  22414  cncls2  22433  cncls  22434  cnntr  22435  cnpresti  22448  cnprest  22449  cnt1  22510  cnhaus  22514  cncmp  22552  cnconn  22582  1stcfb  22605  xkoccn  22779  ptrescn  22799  xkococnlem  22819  qtopeu  22876  qtoprest  22877  kqdisj  22892  kqcldsat  22893  ordthmeolem  22961  fmfnfmlem4  23117  ustuqtoplem  23400  utopsnneiplem  23408  utopsnneip  23409  ucncn  23446  metustto  23718  metustexhalf  23721  metustfbas  23722  cfilucfil  23724  metuust  23725  cfilucfil2  23726  metuel  23729  metuel2  23730  psmetutop  23732  restmetu  23735  metucn  23736  pi1addval  24220  iscph  24343  cphsscph  24424  uniioombllem3  24758  dyadmbl  24773  mbfima  24803  mbfimaicc  24804  mbfimasn  24805  ismbfd  24812  ismbf2d  24813  ismbf3d  24827  mbfimaopnlem  24828  i1fd  24854  i1f1  24863  itg11  24864  i1faddlem  24866  i1fmullem  24867  i1fadd  24868  itg1addlem3  24871  itg1mulc  24878  itg2gt0  24934  limcnlp  25051  ellimc3  25052  limcflf  25054  limciun  25067  mdegval  25237  mdeg0  25244  mdegvsca  25250  mdegpropd  25258  deg1val  25270  ig1pval  25346  coeeu  25395  coeeq  25397  pserulm  25590  areambl  26117  pthdlem2  28145  eupth2lem3  28609  eupth2  28612  issh  29579  isch  29593  shsval  29683  2ndimaxp  30993  fnpreimac  31017  dfcnv2  31022  s2rn  31227  s3rn  31229  swrdrndisj  31238  pwrssmgc  31287  gsummpt2co  31317  gsumpart  31324  gsumhashmul  31325  cycpmco2rn  31401  elrspunidl  31615  rhmimaidl  31618  dimval  31695  dimvalfi  31696  extdgval  31738  smatrcl  31755  locfinreflem  31799  zarclsint  31831  rhmpreimacn  31844  zrhunitpreima  31937  mbfmco2  32241  sibfima  32314  sibfof  32316  eulerpartlemgv  32349  eulerpartlemn  32357  eulerpart  32358  orvcval4  32436  orvcelval  32444  orvcelel  32445  ballotlemscr  32494  fnrelpredd  33070  f1resfz0f1d  33081  pthhashvtx  33098  erdszelem3  33164  erdsze  33173  cvmliftlem3  33258  cvmliftlem7  33262  cvmlift2lem9a  33274  msrval  33509  mvtinf  33526  mclsval  33534  mclsax  33540  mthmpps  33553  opelco3  33758  naddcllem  33840  scutval  34003  madeval  34045  negsval  34132  funpartlem  34253  tailval  34571  ptrest  35785  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem9  35795  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem29  35815  poimirlem31  35817  poimirlem32  35818  mblfinlem2  35824  volsupnfl  35831  itg2addnclem2  35838  sstotbnd2  35941  ismtyhmeolem  35971  grpokerinj  36060  lkrfval  37108  dnnumch3lem  40878  aomclem8  40893  pwfi2f1o  40928  cytpval  41041  frege97d  41367  frege109d  41372  frege131d  41379  nzprmdif  41944  wessf1ornlem  42729  limsuplesup  43247  limsupvaluz  43256  limsuplt2  43301  limsupge  43309  liminfgval  43310  liminfval2  43316  liminflelimsuplem  43323  liminflelimsup  43324  preimaioomnf  44264  fcoreslem2  44569  f1cof1blem  44579  afv2co2  44760  imarnf1pr  44785  preimafvelsetpreimafv  44851  imaelsetpreimafv  44858  imasetpreimafvbijlemfo  44868  fundcmpsurbijinjpreimafv  44870  fundcmpsurinj  44872  fundcmpsurbijinj  44873  isomgr  45286  isomushgr  45289  isomgrsym  45299  isomgrtrlem  45301  predisj  46167