Theorem imaeq2d 5342

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 5338	. 2
3	1, 2	syl 16	1

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

This theorem is referenced by:  imaeq12d  5343  nfimad  5351  csbima12  5359  elimasng  5368  elimasni  5369  csbrn  5473  ressn  5548  foima  5805  f1imacnv  5837  dffv3  5867  fvco2  5948  fsn2  6071  funfvima3  6149  isofrlem  6236  isoselem  6237  fnexALT  6766  curry1  6892  curry2  6895  fparlem3  6902  fparlem4  6903  suppsnop  6932  ressuppssdif  6940  imacosupp  6959  eceq1  7366  uniqs2  7392  ecinxp  7405  mapsn  7480  sbthlem2  7648  sbth  7657  phplem4  7719  php3  7723  marypha1lem  7913  cantnffvalOLD  8103  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  wemapweOLD  8161  oef1oOLD  8163  tcrank  8323  fin4en1  8710  fin1a2lem7  8807  hsmexlem4  8830  hsmexlem5  8831  fpwwe2cbv  9029  fpwwe2lem3  9032  fpwwe2lem13  9041  fpwwecbv  9043  canth4  9046  frnnn0fsupp  10876  limsupgval  13299  isercoll  13490  vdwlem1  14499  vdwlem6  14504  vdwlem7  14505  vdwlem8  14506  vdwlem12  14510  vdwlem13  14511  vdwnn  14516  0ram  14538  ramz2  14542  isacs1i  15054  acsficl  15801  gsumvalx  15897  gsumpropd  15899  gsumpropd2lem  15900  gsumress  15903  efgrelexlema  16767  gsumval3a  16905  gsumval3aOLD  16906  gsumval3lem1  16909  gsumzsubmclOLD  16929  gsum2dlem2  16998  gsum2dOLD  17000  gsum2d2  17002  pwsgsumOLD  17010  dprdvalOLD  17036  dprddisj  17042  dprdf1o  17079  dprdsn  17083  dprd2dlem2  17089  dprd2dlem1  17090  dprd2da  17091  dprd2db  17092  dmdprdsplit2lem  17094  dpjfval  17104  coe1mul2lem2  18309  frlmgsumOLD  18801  frlmup3  18834  islindf  18847  islindf2  18849  lindfind  18851  f1lindf  18857  lmimlbs  18871  subbascn  19755  cncls2  19774  cncls  19775  cnntr  19776  cnpresti  19789  cnprest  19790  cnt1  19851  cnhaus  19855  cncmp  19892  cnconn  19923  1stcfb  19946  xkoccn  20120  ptrescn  20140  xkococnlem  20160  qtopeu  20217  qtoprest  20218  kqdisj  20233  kqcldsat  20234  ordthmeolem  20302  fmfnfmlem4  20458  ustuqtoplem  20742  utopsnneiplem  20750  utopsnneip  20751  ucncn  20788  metusttoOLD  21060  metustto  21061  metustexhalfOLD  21066  metustexhalf  21067  metustfbasOLD  21068  metustfbas  21069  cfilucfilOLD  21072  cfilucfil  21073  metuustOLD  21074  metuust  21075  cfilucfil2OLD  21076  cfilucfil2  21077  metuelOLD  21080  metuel  21081  metuel2  21082  metutopOLD  21085  psmetutop  21086  restmetu  21090  metucnOLD  21091  metucn  21092  pi1addval  21548  iscph  21617  uniioombllem3  21994  dyadmbl  22009  mbfima  22039  mbfimaicc  22040  mbfimasn  22041  ismbfd  22047  ismbf2d  22048  ismbf3d  22061  mbfimaopnlem  22062  i1fd  22088  i1f1  22097  itg11  22098  i1faddlem  22100  i1fmullem  22101  i1fadd  22102  itg1addlem3  22105  itg1mulc  22111  itg2gt0  22167  limcnlp  22282  ellimc3  22283  limcflf  22285  limciun  22298  mdegfvalOLD  22461  mdegval  22462  mdegvalOLD  22463  mdeg0  22470  mdegvsca  22476  mdegpropd  22484  deg1val  22496  ig1pval  22573  coeeu  22622  coeeq  22624  pserulm  22817  areambl  23288  spthispth  24575  1pthonlem2  24592  constr2pth  24603  constr3pthlem3  24657  eupath2lem3  24979  eupath2  24980  efghgrpOLD  25375  issh  26125  isch  26140  shsval  26230  fimacnvinrn2  27476  sspreima  27485  dfcnv2  27517  locfinreflem  27843  zrhunitpreima  27959  mbfmco2  28236  sibfima  28280  sibfof  28282  eulerpartlemgv  28312  eulerpartlemn  28320  eulerpart  28321  orvcval4  28399  orvcelval  28407  orvcelel  28408  ballotlemscr  28457  erdszelem3  28637  erdsze  28646  cvmliftlem3  28732  cvmliftlem7  28736  cvmlift2lem9a  28748  msrval  28898  mvtinf  28915  mclsval  28923  mclsax  28929  mthmpps  28942  opelco3  29208  nofulllem1  29462  nofulllem2  29463  funpartlem  29592  ptrest  30048  mblfinlem2  30052  volsupnfl  30059  itg2addnclem2  30067  tailval  30191  sstotbnd2  30270  ismtyhmeolem  30300  grpokerinj  30347  inisegn0  30989  dnnumch3lem  30992  aomclem8  31007  mapfien2OLD  31042  pwfi2f1o  31044  cytpval  31169  nzprmdif  31224  imarnf1pr  32309  usgra2pthspth  32351  usgra2adedglem1  32356  csbfv12gALTOLD  33621  lkrfval  34812

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-xp 5010  df-cnv 5012  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017