Theorem imaeq1 5337

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
imaeq1

Proof of Theorem imaeq1

Step	Hyp	Ref	Expression
1		reseq1 5272	. . 3
2	1	rneqd 5235	. 2
3		df-ima 5017	. 2
4		df-ima 5017	. 2
5	2, 3, 4	3eqtr4g 2523	1

Syntax hints:  ->wi 4  =wceq 1395  rancrn 5005  |`cres 5006  "cima 5007

This theorem is referenced by:  imaeq1i  5339  imaeq1d  5341  suppval  6920  eceq2  7368  marypha1lem  7913  marypha1  7914  ackbij2lem2  8641  ackbij2lem3  8642  r1om  8645  limsupval  13297  isacs1i  15054  mreacs  15055  islindf  18847  iscnp  19738  xkoccn  20120  xkohaus  20154  xkoco1cn  20158  xkoco2cn  20159  xkococnlem  20160  xkococn  20161  xkoinjcn  20188  fmval  20444  fmf  20446  utoptop  20737  restutop  20740  restutopopn  20741  ustuqtoplem  20742  ustuqtop1  20744  ustuqtop2  20745  ustuqtop4  20747  ustuqtop5  20748  utopsnneiplem  20750  utopsnnei  20752  neipcfilu  20799  metutopOLD  21085  psmetutop  21086  cfilfval  21703  elply2  22593  coeeu  22622  coelem  22623  coeeq  22624  dmarea  23287  mclsax  28929  tailfval  30190  bj-cleq  34519

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