Theorem imaeq1d 5341

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

Hypothesis

Ref	Expression
imaeq1d.1

Assertion

Ref	Expression
imaeq1d

Proof of Theorem imaeq1d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2
2		imaeq1 5337	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  "cima 5007

This theorem is referenced by:  imaeq12d  5343  nfimad  5351  csbrn  5473  f1imacnv  5837  foimacnv  5838  suppssof1OLD  6559  seqomeq12  7138  ssenen  7711  fipreima  7846  oieq1  7958  oieq2  7959  wemapso2OLD  7998  cantnfsOLD  8136  cantnfvalOLD  8138  mapfienOLD  8159  dfac12lem1  8544  dfac12r  8547  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwecbv  9043  fpwwelem  9044  seqeq1  12110  seqeq2  12111  seqeq3  12112  1arith  14445  vdwmc  14496  vdwnnlem1  14513  ramub2  14532  rami  14533  imasless  14937  gsumvalx  15897  eqglact  16252  psgnunilem1  16518  gsumval3OLD  16908  dprdwOLD  17050  rrgsuppOLD  17940  psrbag  18013  psrbagaddclOLD  18021  psrbaglefi  18023  psrbaglefiOLD  18024  mplelbasOLD  18089  mplsubglemOLD  18095  mpllsslemOLD  18096  evlslem4OLD  18173  evlslem6OLD  18182  coe1sfiOLD  18253  evpmss  18622  psgnevpmb  18623  frlmelbasOLD  18789  frlmssuvc1OLD  18827  frlmssuvc2OLD  18828  frlmsslspOLD  18830  frlmup3  18834  ellspdOLD  18837  iscn  19736  ptbasfi  20082  ptval2  20102  ptrescn  20140  xkoptsub  20155  qtopval  20196  cmphaushmeo  20301  ptcmpg  20557  restutopopn  20741  prdsxmslem2  21032  metuvalOLD  21052  metuval  21053  nghmfval  21229  isnghm  21230  ismbf1  22033  ismbf  22037  mbfconst  22042  mbfres2  22052  cncombf  22065  isi1f  22081  itg1val  22090  mdegvalOLD  22463  deg1val  22496  deg1valOLD  22497  fta1glem2  22567  fta1g  22568  fta1b  22570  dgrval  22625  dgrlem  22626  coeidlem  22634  coe11  22650  fta1lem  22703  fta1  22704  vieta1lem2  22707  vieta1  22708  taylthlem2  22769  areaval  23294  sqff1o  23456  nlfnval  26800  fimacnvinrn  27475  xppreima2  27488  ofpreima  27507  fpwrelmapffslem  27555  xrhval  27996  indf1ofs  28039  ismbfm  28223  mbfmcst  28230  issibf  28275  sitgfval  28283  eulerpartlemelr  28296  eulerpartleme  28302  eulerpartlemo  28304  eulerpartlemt0  28308  eulerpartlemt  28310  eulerpartlemr  28313  eulerpartlemgf  28318  eulerpartlemgs2  28319  eulerpartlemn  28320  eulerpart  28321  ballotlemscr  28457  ballotlemrv  28458  ballotlemrinv0  28471  iscvm  28704  cvmliftmolem1  28726  cvmlift2lem9a  28748  cvmlift2lem9  28756  msrfval  28897  ismfs  28909  mthmval  28935  cnambfre  30063  itg2addnclem2  30067  ftc1anclem1  30090  ftc1anclem6  30095  pw2f1o2val  30981  aomclem8  31007  pwfi2f1o  31044  dirkercncflem2  31886  lkrval  34813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-cnv 5012  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017