Theorem imaeq2d 6089

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

Syntax hints:   → wi 4   = wceq 1537   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  imaeq12d  6090  nfimad  6098  csbima12  6108  elimasngOLD  6120  elimasni  6121  inisegn0  6128  csbrn  6234  ressn  6316  csbpredg  6338  predprc  6370  fncofn  6696  foima  6839  focnvimacdmdm  6846  f1imacnv  6878  dffv3  6916  fvco2  7019  sspreima  7101  fimacnvinrn2  7106  rescnvimafod  7107  fsn2  7170  funfvima3  7273  isofrlem  7376  isoselem  7377  fnexALT  7991  mptcnfimad  8027  curry1  8145  curry2  8148  fparlem3  8155  fparlem4  8156  suppsnop  8219  ressuppssdif  8226  suppco  8247  imacosupp  8250  naddcllem  8732  eceq1  8802  uniqs2  8837  ecinxp  8850  mapsnd  8944  sbthlem2  9150  sbth  9159  sbthfi  9265  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  marypha1lem  9502  cantnfp1lem3  9749  tcrank  9953  fin4en1  10378  fin1a2lem7  10475  hsmexlem4  10498  hsmexlem5  10499  fpwwe2cbv  10699  fpwwe2lem3  10702  fpwwe2lem12  10711  fpwwecbv  10713  canth4  10716  resunimafz0  14494  limsupgval  15522  isercoll  15716  vdwlem1  17028  vdwlem6  17033  vdwlem7  17034  vdwlem8  17035  vdwlem12  17039  vdwlem13  17040  vdwnn  17045  0ram  17067  ramz2  17071  isacs1i  17715  acsficl  18617  gsumvalx  18714  gsumpropd  18716  gsumpropd2lem  18717  gsumress  18720  efgrelexlema  19791  gsumval3a  19945  gsumval3lem1  19947  gsum2dlem2  20013  gsum2d2  20016  dprddisj  20053  dprdf1o  20076  dprdsn  20080  dprd2dlem2  20084  dprd2dlem1  20085  dprd2da  20086  dprd2db  20087  dmdprdsplit2lem  20089  dpjfval  20099  rngqiprngimf1  21333  frlmup3  21843  islindf  21855  islindf2  21857  lindfind  21859  f1lindf  21865  lmimlbs  21879  coe1mul2lem2  22292  subbascn  23283  cncls2  23302  cncls  23303  cnntr  23304  cnpresti  23317  cnprest  23318  cnt1  23379  cnhaus  23383  cncmp  23421  cnconn  23451  1stcfb  23474  xkoccn  23648  ptrescn  23668  xkococnlem  23688  qtopeu  23745  qtoprest  23746  kqdisj  23761  kqcldsat  23762  ordthmeolem  23830  fmfnfmlem4  23986  ustuqtoplem  24269  utopsnneiplem  24277  utopsnneip  24278  ucncn  24315  metustto  24587  metustexhalf  24590  metustfbas  24591  cfilucfil  24593  metuust  24594  cfilucfil2  24595  metuel  24598  metuel2  24599  psmetutop  24601  restmetu  24604  metucn  24605  pi1addval  25100  iscph  25223  cphsscph  25304  uniioombllem3  25639  dyadmbl  25654  mbfima  25684  mbfimaicc  25685  mbfimasn  25686  ismbfd  25693  ismbf2d  25694  ismbf3d  25708  mbfimaopnlem  25709  i1fd  25735  i1f1  25744  itg11  25745  i1faddlem  25747  i1fmullem  25748  i1fadd  25749  itg1addlem3  25752  itg1mulc  25759  itg2gt0  25815  limcnlp  25933  ellimc3  25934  limcflf  25936  limciun  25949  mdegval  26122  mdeg0  26129  mdegvsca  26135  mdegpropd  26143  deg1val  26155  ig1pval  26235  coeeu  26284  coeeq  26286  pserulm  26483  areambl  27019  scutval  27863  madeval  27909  addsbday  28068  negsval  28075  pthdlem2  29804  eupth2lem3  30268  eupth2  30271  issh  31240  isch  31254  shsval  31344  2ndimaxp  32665  fnpreimac  32689  dfcnv2  32694  mptiffisupp  32705  s2rnOLD  32910  s3rnOLD  32912  swrdrndisj  32924  pwrssmgc  32973  gsummpt2co  33031  gsumpart  33038  gsumhashmul  33040  cycpmco2rn  33118  qusrn  33402  elrspunidl  33421  rhmimaidl  33425  r1pquslmic  33596  dimval  33613  dimvalfi  33614  ply1degltdimlem  33635  extdgval  33667  algextdeglem3  33710  algextdeglem4  33711  algextdeglem5  33712  smatrcl  33742  locfinreflem  33786  zarclsint  33818  rhmpreimacn  33831  zrhunitpreima  33924  mbfmco2  34230  sibfima  34303  sibfof  34305  eulerpartlemgv  34338  eulerpartlemn  34346  eulerpart  34347  orvcval4  34425  orvcelval  34433  orvcelel  34434  ballotlemscr  34483  fnrelpredd  35065  f1resfz0f1d  35081  pthhashvtx  35095  erdszelem3  35161  erdsze  35170  cvmliftlem3  35255  cvmliftlem7  35259  cvmlift2lem9a  35271  msrval  35506  mvtinf  35523  mclsval  35531  mclsax  35537  mthmpps  35550  opelco3  35738  funpartlem  35906  tailval  36339  ptrest  37579  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  volsupnfl  37625  itg2addnclem2  37632  sstotbnd2  37734  ismtyhmeolem  37764  grpokerinj  37853  lkrfval  39043  aks6d1c6lem5  42134  aks6d1c7lem3  42139  dnnumch3lem  43003  aomclem8  43018  pwfi2f1o  43053  cytpval  43163  frege97d  43714  frege109d  43719  frege131d  43726  nzprmdif  44288  wessf1ornlem  45092  limsuplesup  45620  limsupvaluz  45629  limsuplt2  45674  limsupge  45682  liminfgval  45683  liminfval2  45689  liminflelimsuplem  45696  liminflelimsup  45697  preimaioomnf  46640  fcoreslem2  46979  f1cof1blem  46989  3f1oss1  46990  afv2co2  47172  imarnf1pr  47197  preimafvelsetpreimafv  47262  imaelsetpreimafv  47269  imasetpreimafvbijlemfo  47279  fundcmpsurbijinjpreimafv  47281  fundcmpsurinj  47283  fundcmpsurbijinj  47284  isgrim  47752  isuspgrim0lem  47755  isuspgrim0  47756  grimuhgr  47762  grimcnv  47763  grimco  47764  gricushgr  47770  isubgrgrim  47781  uhgrimisgrgriclem  47782  clnbgrgrimlem  47785  clnbgrgrim  47786  grimedg  47787  uspgrlimlem3  47814  predisj  48542