Theorem imaeq1i 5339

Description: Equality theorem for image. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
imaeq1i.1

Assertion

Ref	Expression
imaeq1i

Proof of Theorem imaeq1i

Step	Hyp	Ref	Expression
1		imaeq1i.1	. 2
2		imaeq1 5337	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  "cima 5007

This theorem is referenced by:  mptpreima  5505  isarep2  5673  suppun  6939  supp0cosupp0  6958  imacosupp  6959  fsuppun  7868  fsuppcolem  7880  marypha2lem4  7918  dfoi  7957  mapfienOLD  8159  r1limg  8210  isf34lem3  8776  compss  8777  fpwwe2lem13  9041  infmsup  10546  gsumval3OLD  16908  gsumzf1o  16917  gsumzf1oOLD  16920  gsumzaddlemOLD  16936  dprdfidOLD  17064  funsnfsupOLD  18256  ssidcn  19756  cnco  19767  qtopres  20199  idqtop  20207  qtopcn  20215  mbfid  22043  mbfres  22051  cncombf  22065  dvlog  23032  efopnlem2  23038  disjpreima  27445  imadifxp  27458  rinvf1o  27472  mbfmcst  28230  mbfmco  28235  eulerpartlemt  28310  eulerpartlemmf  28314  eulerpart  28321  0rrv  28390  mclsppslem  28943  ftc1anclem3  30092  areacirclem5  30111  cytpval  31169  arearect  31183  0cnf  31679  mbf0  31756  fourierdlem62  31951

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