Theorem imaeq2d 6068

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-xp 5662  df-cnv 5664  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669

This theorem is used by:  imaeq12d  6069  nfimad  6081  csbima12  6092  elimasni  6105  inisegn0  6112  csbrn  6221  ressn  6310  csbpredg  6334  predprc  6365  fncofn  6684  foima  6829  focnvimacdmdm  6836  f1imacnv  6869  dffv3  6910  fvco2  7011  sspreima  7097  fimacnvinrn2  7102  rescnvimafod  7103  fsn2  7167  funfvima3  7271  isofrlem  7377  isoselem  7378  fnexALT  7995  mptcnfimad  8030  curry1  8150  curry2  8153  fparlem3  8160  fparlem4  8161  suppsnop  8231  ressuppssdif  8238  suppco  8259  imacosupp  8262  naddcllem  8721  eceq1  8793  uniqs2  8833  ecinxp  8849  mapsnd  8950  sbthlem2  9143  sbth  9152  sbthfi  9250  phplem2  9256  php3  9260  marypha1lem  9460  cantnfp1lem3  9716  tcrank  9936  fin4en1  10424  fin1a2lem7  10521  hsmexlem4  10544  hsmexlem5  10545  fpwwe2cbv  10752  fpwwe2lem3  10755  fpwwe2lem12  10764  fpwwecbv  10766  canth4  10769  f1resfz0f1d  13965  resunimafz0  14629  limsupgval  15684  isercoll  15876  vdwlem1  17200  vdwlem6  17205  vdwlem7  17206  vdwlem8  17207  vdwlem12  17211  vdwlem13  17212  vdwnn  17217  0ram  17239  ramz2  17243  isacs1i  17872  acsficl  18762  gsumvalx  18906  gsumpropd  18908  gsumpropd2lem  18909  gsumress  18912  efgrelexlema  20005  gsumval3a  20159  gsumval3lem1  20161  gsum2dlem2  20227  gsum2d2  20230  dprddisj  20267  dprdf1o  20290  dprdsn  20294  dprd2dlem2  20298  dprd2dlem1  20299  dprd2da  20300  dprd2db  20301  dmdprdsplit2lem  20303  dpjfval  20313  rngqiprngimf1  21638  frlmup3  22150  islindf  22162  islindf2  22164  lindfind  22166  f1lindf  22172  lmimlbs  22186  coe1mul2lem2  22631  subbascn  23616  cncls2  23635  cncls  23636  cnntr  23637  cnpresti  23650  cnprest  23651  cnt1  23712  cnhaus  23716  cncmp  23754  cnconn  23784  1stcfb  23807  xkoccn  23982  ptrescn  24002  xkococnlem  24022  qtopeu  24079  qtoprest  24080  kqdisj  24095  kqcldsat  24096  ordthmeolem  24164  fmfnfmlem4  24320  ustuqtoplem  24602  utopsnneiplem  24610  utopsnneip  24611  ucncn  24647  metustto  24916  metustexhalf  24919  metustfbas  24920  cfilucfil  24922  metuust  24923  cfilucfil2  24924  metuel  24927  metuel2  24928  psmetutop  24930  restmetu  24933  metucn  24934  pi1addval  25413  iscph  25535  cphsscph  25616  uniioombllem3  25950  dyadmbl  25965  mbfima  25995  mbfimaicc  25996  mbfimasn  25997  ismbfd  26004  ismbf2d  26005  ismbf3d  26019  mbfimaopnlem  26020  i1fd  26046  i1f1  26055  itg11  26056  i1faddlem  26058  i1fmullem  26059  i1fadd  26060  itg1addlem3  26063  itg1mulc  26069  itg2gt0  26125  limcnlp  26242  ellimc3  26243  limcflf  26245  limciun  26258  mdegval  26425  mdeg0  26432  mdegvsca  26438  mdegpropd  26446  deg1val  26458  ig1pval  26538  coeeu  26588  coeeq  26590  pserulm  26795  areambl  27332  cutsval  28212  madeval  28264  addbday  28450  negsval  28457  bdayons  28708  zcuts0  28840  bdaypw2n0bndlem  28895  dfpth2  30360  pthhashvtx  30361  pthdlem2  30400  cyclnumvtx  30434  eupth2lem3  30883  eupth2  30886  issh  31856  isch  31870  shsval  31960  2ndimaxp  33328  fnpreimac  33352  dfcnv2  33356  mptiffisupp  33373  indsupp  33520  indfsid  33522  swrdrndisj  33604  pwrssmgc  33650  gsummpt2co  33698  gsumpart  33713  gsumhashmul  33717  cycpmco2rn  33775  qusrn  34057  elrspunidl  34075  rhmimaidl  34079  r1pquslmic  34240  psrbasfsupp  34247  esplyfval  34299  esplyfval0  34300  esplyfval2  34301  vieta  34316  dimval  34337  dimvalfi  34338  ply1degltdimlem  34358  extdgval  34389  algextdeglem3  34455  algextdeglem4  34456  algextdeglem5  34457  smatrcl  34532  locfinreflem  34576  zarclsint  34608  rhmpreimacn  34621  zrhunitpreima  34712  mbfmco2  35001  sibfima  35074  sibfof  35076  eulerpartlemgv  35109  eulerpartlemn  35117  eulerpart  35118  orvcval4  35197  orvcelval  35205  orvcelel  35206  ballotlemscr  35255  fnrelpredd  35838  fineqvhfbregs  35940  onvfowev  36084  erdszelem3  36159  erdsze  36168  cvmliftlem3  36253  cvmliftlem7  36257  cvmlift2lem9a  36269  msrval  36504  mvtinf  36521  mclsval  36529  mclsax  36535  mthmpps  36548  opelco3  36747  funpartlem  36914  tailval  37369  ptrest  38798  poimirlem1  38800  poimirlem2  38801  poimirlem3  38802  poimirlem4  38803  poimirlem5  38804  poimirlem6  38805  poimirlem7  38806  poimirlem9  38808  poimirlem10  38809  poimirlem11  38810  poimirlem12  38811  poimirlem13  38812  poimirlem14  38813  poimirlem15  38814  poimirlem16  38815  poimirlem17  38816  poimirlem19  38818  poimirlem20  38819  poimirlem22  38821  poimirlem23  38822  poimirlem24  38823  poimirlem25  38824  poimirlem26  38825  poimirlem27  38826  poimirlem28  38827  poimirlem29  38828  poimirlem31  38830  poimirlem32  38831  mblfinlem2  38837  volsupnfl  38844  itg2addnclem2  38851  sstotbnd2  38967  ismtyhmeolem  38997  grpokerinj  39086  lkrfval  40403  aks6d1c6lem5  43486  aks6d1c7lem3  43491  dnnumch3lem  44313  aomclem8  44323  pwfi2f1o  44358  cytpval  44459  frege97d  45007  frege109d  45012  frege131d  45019  nzprmdif  45558  relpfrlem  46201  wessf1ornlem  46467  limsuplesup  46976  limsupvaluz  46985  limsuplt2  47030  limsupge  47038  liminfgval  47039  liminfval2  47045  liminflelimsuplem  47052  liminflelimsup  47053  preimaioomnf  47996  tmachlem-agreefin  48225  tmachlem-franscan  48226  fcoreslem2  48401  f1cof1blem  48411  3f1oss1  48412  afv2co2  48594  imarnf1pr  48619  preimafvelsetpreimafv  48737  imaelsetpreimafv  48744  imasetpreimafvbijlemfo  48754  fundcmpsurbijinjpreimafv  48756  fundcmpsurinj  48758  fundcmpsurbijinj  48759  isgrim  49247  grimuhgr  49252  grimcnv  49253  grimco  49254  uhgrimedgi  49255  isuspgrim0lem  49258  isuspgrim0  49259  upgrimwlklem3  49264  upgrimtrls  49271  upgrimpths  49274  gricushgr  49282  cycldlenngric  49293  isubgrgrim  49294  uhgrimisgrgriclem  49295  clnbgrgrimlem  49298  clnbgrgrim  49299  grimedg  49300  cycl3grtri  49312  isubgr3stgrlem4  49334  uspgrlimlem3  49355  predisj  50246  imasubclem3  50547