Theorem imaeq1d 5465

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

Hypothesis

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

Assertion

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

Proof of Theorem imaeq1d

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

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-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  imaeq12d  5467  nfimad  5475  csbrn  5596  f1imacnv  6153  foimacnv  6154  fimacnvinrn  6348  seqomeq12  7549  ssenen  8134  fipreima  8272  oieq1  8417  oieq2  8418  dfac12lem1  8965  dfac12r  8968  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwecbv  9466  fpwwelem  9467  seqeq1  12804  seqeq2  12805  seqeq3  12806  1arith  15631  vdwmc  15682  vdwnnlem1  15699  ramub2  15718  rami  15719  imasless  16200  gsumvalx  17270  eqglact  17645  psgnunilem1  17913  psrbag  19364  psrbaglefi  19372  evpmss  19932  psgnevpmb  19933  frlmup3  20139  iscn  21039  ptbasfi  21384  ptval2  21404  ptrescn  21442  xkoptsub  21457  qtopval  21498  cmphaushmeo  21603  ptcmpg  21861  restutopopn  22042  prdsxmslem2  22334  metuval  22354  nghmfval  22526  isnghm  22527  ismbf1  23393  ismbf  23397  mbfconst  23402  mbfres2  23412  cncombf  23425  isi1f  23441  itg1val  23450  deg1val  23856  fta1glem2  23926  fta1g  23927  fta1b  23929  dgrval  23984  dgrlem  23985  coeidlem  23993  coe11  24009  fta1lem  24062  fta1  24063  vieta1lem2  24066  vieta1  24067  taylthlem2  24128  areaval  24691  sqff1o  24908  nlfnval  28740  xppreima2  29450  ofpreima  29465  fpwrelmapffslem  29507  xrhval  30062  indf1ofs  30088  ismbfm  30314  mbfmcst  30321  issibf  30395  sitgfval  30403  eulerpartlemelr  30419  eulerpartleme  30425  eulerpartlemo  30427  eulerpartlemt0  30431  eulerpartlemt  30433  eulerpartlemr  30436  eulerpartlemgf  30441  eulerpartlemgs2  30442  eulerpartlemn  30443  eulerpart  30444  ballotlemscr  30580  ballotlemrv  30581  ballotlemrinv0  30594  iscvm  31241  cvmliftmolem1  31263  cvmlift2lem9a  31285  cvmlift2lem9  31293  msrfval  31434  ismfs  31446  mthmval  31472  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem26  33435  poimirlem27  33436  poimirlem32  33441  cnambfre  33458  itg2addnclem2  33462  ftc1anclem1  33485  ftc1anclem6  33490  lkrval  34375  pw2f1o2val  37606  aomclem8  37631  pwfi2f1o  37666  trclimalb2  38018  frege131d  38056  dirkercncflem2  40321  issmflem  40936  smfpimioo  40994  smfpimcc  41014  smfsuplem2  41018