Theorem imaeq2 5338

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

Assertion

Ref	Expression
imaeq2

Proof of Theorem imaeq2

Step	Hyp	Ref	Expression
1		reseq2 5273	. . 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:  imaeq2i  5340  imaeq2d  5342  relimasn  5365  funimaexg  5670  ssimaex  5938  ssimaexg  5939  isoselem  6237  isowe2  6246  f1opw2  6528  fnse  6917  supp0cosupp0  6958  tz7.49  7129  ecexr  7335  fopwdom  7645  sbthlem2  7648  sbth  7657  ssenen  7711  domunfican  7813  fodomfi  7819  f1opwfi  7844  fipreima  7846  marypha1lem  7913  ordtypelem2  7965  ordtypelem3  7966  ordtypelem9  7972  dfac12lem2  8545  dfac12r  8547  ackbij2lem2  8641  ackbij2lem3  8642  r1om  8645  enfin2i  8722  zorn2lem6  8902  zorn2lem7  8903  isacs5lem  15799  acsdrscl  15800  gicsubgen  16326  efgrelexlema  16767  gsumval3OLD  16908  tgcn  19753  subbascn  19755  iscnp4  19764  cnpnei  19765  cnima  19766  iscncl  19770  cncls  19775  cnconst2  19784  cnrest2  19787  cnprest  19790  cnindis  19793  cncmp  19892  cmpfi  19908  2ndcomap  19959  ptbasfi  20082  xkoopn  20090  xkoccn  20120  txcnp  20121  ptcnplem  20122  txcnmpt  20125  ptrescn  20140  xkoco1cn  20158  xkoco2cn  20159  xkococn  20161  xkoinjcn  20188  elqtop  20198  qtopomap  20219  qtopcmap  20220  ordthmeolem  20302  fbasrn  20385  elfm  20448  elfm2  20449  elfm3  20451  imaelfm  20452  rnelfmlem  20453  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem3  20457  fmfnfmlem4  20458  fmco  20462  flffbas  20496  lmflf  20506  fcfneii  20538  ptcmplem3  20554  ptcmplem5  20556  ptcmpg  20557  cnextcn  20567  symgtgp  20600  ghmcnp  20613  eltsms  20631  tsmsf1o  20647  fmucnd  20795  ucnextcn  20807  metcnp3  21043  mbfdm  22035  ismbf  22037  mbfima  22039  ismbfd  22047  mbfimaopnlem  22062  mbfimaopn2  22064  i1fd  22088  ellimc2  22281  limcflf  22285  xrlimcnp  23298  ubthlem1  25786  disjpreima  27445  imadifxp  27458  qtophaus  27839  rrhre  27999  mbfmcnvima  28228  imambfm  28233  eulerpartgbij  28311  erdszelem1  28635  erdsze  28646  erdsze2lem2  28648  cvmscbv  28703  cvmsi  28710  cvmsval  28711  cvmliftlem15  28743  opelco3  29208  brimageg  29577  fnimage  29579  imageval  29580  fvimage  29581  ptrest  30048  filnetlem4  30199  ismtyhmeolem  30300  ismtybndlem  30302  heibor1lem  30305  lmhmfgima  31030  icccncfext  31690  csbfv12gALTVD  33699

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