Theorem imaeq2d 6056

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  imaeq12d  6057  nfimad  6065  csbima12  6075  elimasni  6087  inisegn0  6094  csbrn  6199  ressn  6283  csbpredg  6305  predprc  6336  fncofn  6649  foima  6794  focnvimacdmdm  6801  f1imacnv  6834  dffv3  6874  fvco2  6975  sspreima  7060  fimacnvinrn2  7065  rescnvimafod  7066  fsn2  7130  funfvima3  7235  isofrlem  7341  isoselem  7342  fnexALT  7948  mptcnfimad  7983  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  8893  sbthlem2  9086  sbth  9095  sbthfi  9193  phplem2  9199  php3  9203  marypha1lem  9403  cantnfp1lem3  9659  tcrank  9866  fin4en1  10311  fin1a2lem7  10408  hsmexlem4  10431  hsmexlem5  10432  fpwwe2cbv  10639  fpwwe2lem3  10642  fpwwe2lem12  10651  fpwwecbv  10653  canth4  10656  f1resfz0f1d  13848  resunimafz0  14510  limsupgval  15563  isercoll  15755  vdwlem1  17073  vdwlem6  17078  vdwlem7  17079  vdwlem8  17080  vdwlem12  17084  vdwlem13  17085  vdwnn  17090  0ram  17112  ramz2  17116  isacs1i  17745  acsficl  18635  gsumvalx  18778  gsumpropd  18780  gsumpropd2lem  18781  gsumress  18784  efgrelexlema  19876  gsumval3a  20030  gsumval3lem1  20032  gsum2dlem2  20098  gsum2d2  20101  dprddisj  20138  dprdf1o  20161  dprdsn  20165  dprd2dlem2  20169  dprd2dlem1  20170  dprd2da  20171  dprd2db  20172  dmdprdsplit2lem  20174  dpjfval  20184  rngqiprngimf1  21503  frlmup3  22013  islindf  22025  islindf2  22027  lindfind  22029  f1lindf  22035  lmimlbs  22049  coe1mul2lem2  22494  subbascn  23479  cncls2  23498  cncls  23499  cnntr  23500  cnpresti  23513  cnprest  23514  cnt1  23575  cnhaus  23579  cncmp  23617  cnconn  23647  1stcfb  23670  xkoccn  23845  ptrescn  23865  xkococnlem  23885  qtopeu  23942  qtoprest  23943  kqdisj  23958  kqcldsat  23959  ordthmeolem  24027  fmfnfmlem4  24183  ustuqtoplem  24465  utopsnneiplem  24473  utopsnneip  24474  ucncn  24510  metustto  24779  metustexhalf  24782  metustfbas  24783  cfilucfil  24785  metuust  24786  cfilucfil2  24787  metuel  24790  metuel2  24791  psmetutop  24793  restmetu  24796  metucn  24797  pi1addval  25276  iscph  25398  cphsscph  25479  uniioombllem3  25813  dyadmbl  25828  mbfima  25858  mbfimaicc  25859  mbfimasn  25860  ismbfd  25867  ismbf2d  25868  ismbf3d  25882  mbfimaopnlem  25883  i1fd  25909  i1f1  25918  itg11  25919  i1faddlem  25921  i1fmullem  25922  i1fadd  25923  itg1addlem3  25926  itg1mulc  25932  itg2gt0  25988  limcnlp  26105  ellimc3  26106  limcflf  26108  limciun  26121  mdegval  26288  mdeg0  26295  mdegvsca  26301  mdegpropd  26309  deg1val  26321  ig1pval  26401  coeeu  26451  coeeq  26453  pserulm  26658  areambl  27195  cutsval  28045  madeval  28097  addbday  28283  negsval  28290  bdayons  28541  zcuts0  28673  bdaypw2n0bndlem  28728  dfpth2  30193  pthhashvtx  30194  pthdlem2  30233  cyclnumvtx  30267  eupth2lem3  30716  eupth2  30719  issh  31689  isch  31703  shsval  31793  2ndimaxp  33119  fnpreimac  33143  dfcnv2  33148  mptiffisupp  33165  indsupp  33313  indfsid  33315  swrdrndisj  33397  pwrssmgc  33440  gsummpt2co  33488  gsumpart  33503  gsumhashmul  33507  cycpmco2rn  33565  qusrn  33838  elrspunidl  33856  rhmimaidl  33860  r1pquslmic  34020  psrbasfsupp  34021  esplyfval  34073  esplyfval0  34074  esplyfval2  34075  vieta  34090  dimval  34111  dimvalfi  34112  ply1degltdimlem  34132  extdgval  34163  algextdeglem3  34229  algextdeglem4  34230  algextdeglem5  34231  smatrcl  34306  locfinreflem  34350  zarclsint  34382  rhmpreimacn  34395  zrhunitpreima  34486  mbfmco2  34776  sibfima  34849  sibfof  34851  eulerpartlemgv  34884  eulerpartlemn  34892  eulerpart  34893  orvcval4  34972  orvcelval  34980  orvcelel  34981  ballotlemscr  35030  fnrelpredd  35596  fineqvr1ombregs  35664  onvfowev  35713  erdszelem3  35772  erdsze  35781  cvmliftlem3  35866  cvmliftlem7  35870  cvmlift2lem9a  35882  msrval  36117  mvtinf  36134  mclsval  36142  mclsax  36148  mthmpps  36161  opelco3  36354  funpartlem  36521  tailval  36992  ptrest  38368  poimirlem1  38370  poimirlem2  38371  poimirlem3  38372  poimirlem4  38373  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem9  38378  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem22  38391  poimirlem23  38392  poimirlem24  38393  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  poimirlem28  38397  poimirlem29  38398  poimirlem31  38400  poimirlem32  38401  mblfinlem2  38407  volsupnfl  38414  itg2addnclem2  38421  sstotbnd2  38524  ismtyhmeolem  38554  grpokerinj  38643  lkrfval  39960  aks6d1c6lem5  43043  aks6d1c7lem3  43048  dnnumch3lem  43887  aomclem8  43902  pwfi2f1o  43937  cytpval  44043  frege97d  44592  frege109d  44597  frege131d  44604  nzprmdif  45143  relpfrlem  45776  wessf1ornlem  46017  limsuplesup  46527  limsupvaluz  46536  limsuplt2  46581  limsupge  46589  liminfgval  46590  liminfval2  46596  liminflelimsuplem  46603  liminflelimsup  46604  preimaioomnf  47547  tmachlem-agreefin  47776  tmachlem-franscan  47777  fcoreslem2  47952  f1cof1blem  47962  3f1oss1  47963  afv2co2  48145  imarnf1pr  48170  preimafvelsetpreimafv  48288  imaelsetpreimafv  48295  imasetpreimafvbijlemfo  48305  fundcmpsurbijinjpreimafv  48307  fundcmpsurinj  48309  fundcmpsurbijinj  48310  isgrim  48798  grimuhgr  48803  grimcnv  48804  grimco  48805  uhgrimedgi  48806  isuspgrim0lem  48809  isuspgrim0  48810  upgrimwlklem3  48815  upgrimtrls  48822  upgrimpths  48825  gricushgr  48833  cycldlenngric  48844  isubgrgrim  48845  uhgrimisgrgriclem  48846  clnbgrgrimlem  48849  clnbgrgrim  48850  grimedg  48851  cycl3grtri  48863  isubgr3stgrlem4  48885  uspgrlimlem3  48906  predisj  49739  imasubclem3  50032