Theorem imaeq2d 5466

Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Hypothesis

Ref	Expression
imaeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
imaeq2d	|- ( ph -> ( C " A ) = ( C " B ) )

Proof of Theorem imaeq2d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2 |- ( ph -> A = B )
2		imaeq2 5462	. 2 |- ( A = B -> ( C " A ) = ( C " B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C " A ) = ( C " B ) )

Syntax hints:   -> wi 4   = wceq 1483   "cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  imaeq12d  5467  nfimad  5475  csbima12  5483  elimasng  5491  elimasni  5492  inisegn0  5497  csbrn  5596  ressn  5671  foima  6120  f1imacnv  6153  dffv3  6187  fvco2  6273  fimacnvinrn2  6349  fsn2  6403  funfvima3  6495  isofrlem  6590  isoselem  6591  fnexALT  7132  curry1  7269  curry2  7272  fparlem3  7279  fparlem4  7280  suppsnop  7309  ressuppssdif  7316  imacosupp  7335  eceq1  7782  uniqs2  7809  ecinxp  7822  mapsn  7899  sbthlem2  8071  sbth  8080  phplem4  8142  php3  8146  marypha1lem  8339  cantnfp1lem3  8577  tcrank  8747  fin4en1  9131  fin1a2lem7  9228  hsmexlem4  9251  hsmexlem5  9252  fpwwe2cbv  9452  fpwwe2lem3  9455  fpwwe2lem13  9464  fpwwecbv  9466  canth4  9469  frnnn0fsupp  11350  resunimafz0  13229  limsupgval  14207  isercoll  14398  vdwlem1  15685  vdwlem6  15690  vdwlem7  15691  vdwlem8  15692  vdwlem12  15696  vdwlem13  15697  vdwnn  15702  0ram  15724  ramz2  15728  isacs1i  16318  acsficl  17171  gsumvalx  17270  gsumpropd  17272  gsumpropd2lem  17273  gsumress  17276  efgrelexlema  18162  gsumval3a  18304  gsumval3lem1  18306  gsum2dlem2  18370  gsum2d2  18373  dprddisj  18408  dprdf1o  18431  dprdsn  18435  dprd2dlem2  18439  dprd2dlem1  18440  dprd2da  18441  dprd2db  18442  dmdprdsplit2lem  18444  dpjfval  18454  coe1mul2lem2  19638  frlmup3  20139  islindf  20151  islindf2  20153  lindfind  20155  f1lindf  20161  lmimlbs  20175  subbascn  21058  cncls2  21077  cncls  21078  cnntr  21079  cnpresti  21092  cnprest  21093  cnt1  21154  cnhaus  21158  cncmp  21195  cnconn  21225  1stcfb  21248  xkoccn  21422  ptrescn  21442  xkococnlem  21462  qtopeu  21519  qtoprest  21520  kqdisj  21535  kqcldsat  21536  ordthmeolem  21604  fmfnfmlem4  21761  ustuqtoplem  22043  utopsnneiplem  22051  utopsnneip  22052  ucncn  22089  metustto  22358  metustexhalf  22361  metustfbas  22362  cfilucfil  22364  metuust  22365  cfilucfil2  22366  metuel  22369  metuel2  22370  psmetutop  22372  restmetu  22375  metucn  22376  pi1addval  22848  iscph  22970  uniioombllem3  23353  dyadmbl  23368  mbfima  23399  mbfimaicc  23400  mbfimasn  23401  ismbfd  23407  ismbf2d  23408  ismbf3d  23421  mbfimaopnlem  23422  i1fd  23448  i1f1  23457  itg11  23458  i1faddlem  23460  i1fmullem  23461  i1fadd  23462  itg1addlem3  23465  itg1mulc  23471  itg2gt0  23527  limcnlp  23642  ellimc3  23643  limcflf  23645  limciun  23658  mdegval  23823  mdeg0  23830  mdegvsca  23836  mdegpropd  23844  deg1val  23856  ig1pval  23932  coeeu  23981  coeeq  23983  pserulm  24176  areambl  24685  pthdlem2  26664  eupth2lem3  27096  eupth2  27099  issh  28065  isch  28079  shsval  28171  sspreima  29447  dfcnv2  29476  gsummpt2co  29780  smatrcl  29862  locfinreflem  29907  zrhunitpreima  30022  mbfmco2  30327  sibfima  30400  sibfof  30402  eulerpartlemgv  30435  eulerpartlemn  30443  eulerpart  30444  orvcval4  30522  orvcelval  30530  orvcelel  30531  ballotlemscr  30580  erdszelem3  31175  erdsze  31184  cvmliftlem3  31269  cvmliftlem7  31273  cvmlift2lem9a  31285  msrval  31435  mvtinf  31452  mclsval  31460  mclsax  31466  mthmpps  31479  opelco3  31678  scutval  31911  madeval  31935  funpartlem  32049  tailval  32368  csbpredg  33172  ptrest  33408  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  mblfinlem2  33447  volsupnfl  33454  itg2addnclem2  33462  sstotbnd2  33573  ismtyhmeolem  33603  grpokerinj  33692  lkrfval  34374  dnnumch3lem  37616  aomclem8  37631  pwfi2f1o  37666  cytpval  37787  frege97d  38044  frege109d  38049  frege131d  38056  nzprmdif  38518  csbfv12gALTOLD  39052  wessf1ornlem  39371  mapsnd  39388  limsuplesup  39931  limsupvaluz  39940  limsuplt2  39985  limsupge  39993  liminfgval  39994  liminfval2  40000  liminflelimsuplem  40007  liminflelimsup  40008  preimaioomnf  40929  imarnf1pr  41301