Theorem imassrn 5353

Description: The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.)

Assertion

Ref	Expression
imassrn

Proof of Theorem imassrn

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		exsimpr 1678	. . 3
2	1	ss2abi 3571	. 2
3		dfima3 5345	. 2
4		dfrn3 5197	. 2
5	2, 3, 4	3sstr4i 3542	1

Syntax hints:  /\wa 369  E.wex 1612  e.wcel 1818  {cab 2442  C_wss 3475  <.cop 4035  rancrn 5005  "cima 5007

This theorem is referenced by:  0ima  5358  cnvimass  5362  fimacnv  6019  isofrlem  6236  isofr2  6240  f1opw2  6528  imaexg  6737  f1oweALT  6784  frxp  6910  smores2  7044  ecss  7372  f1imaen2g  7596  domunsncan  7637  fopwdom  7645  sbthlem2  7648  sbthlem3  7649  sbthlem5  7651  sbthlem6  7652  ssenen  7711  ssfi  7760  fiint  7817  f1opwfi  7844  fissuni  7845  fipreima  7846  marypha1lem  7913  unxpwdom2  8035  tz9.12lem1  8226  acndom2  8456  dfac12lem2  8545  isf34lem5  8779  isf34lem7  8780  isf34lem6  8781  enfin1ai  8785  hsmexlem4  8830  hsmexlem5  8831  fpwwe2lem6  9034  fpwwe2lem9  9037  tskuni  9182  limsupgle  13300  limsupval2  13303  limsupgre  13304  isercolllem2  13488  isercoll  13490  unbenlem  14426  imasless  14937  isacs1i  15054  isacs4lem  15798  mhmima  15994  cntzmhm  16376  f1omvdconj  16471  psgnunilem1  16518  gsumzaddlem  16934  gsumzaddlemOLD  16936  dmdprdd  17030  dprdfeq0  17062  dprdfeq0OLD  17069  dprdres  17075  dprdss  17076  dprdz  17077  subgdmdprd  17081  dprd2dlem1  17090  dprd2da  17091  dmdprdsplit2lem  17094  lmhmlsp  17695  funsnfsupOLD  18256  frlmsslsp  18829  frlmsslspOLD  18830  lindff1  18855  lindfrn  18856  f1lindf  18857  lindfmm  18862  lsslindf  18865  cnclsi  19773  cnprest2  19791  paste  19795  cmpfi  19908  conima  19926  1stcfb  19946  1stckgenlem  20054  kgencn3  20059  xkoco1cn  20158  xkoco2cn  20159  xkococnlem  20160  qtopval2  20197  basqtop  20212  imastopn  20221  kqopn  20235  kqcld  20236  hmeontr  20270  hmeores  20272  hmphdis  20297  cmphaushmeo  20301  qtopf1  20317  fbasrn  20385  uzfbas  20399  elfm  20448  elfm3  20451  imaelfm  20452  rnelfm  20454  cnextcn  20567  tgpconcomp  20611  qustgpopn  20618  tsmsf1o  20647  ustimasn  20731  utopbas  20738  restutop  20740  qtopbaslem  21265  tgqioo  21305  cnheiborlem  21454  bndth  21458  fmcfil  21711  ovoliunlem1  21913  volsup  21966  uniioombllem4  21995  uniioombllem5  21996  opnmblALT  22012  volsup2  22014  mbfimaopnlem  22062  mbflimsup  22073  itg2gt0  22167  c1liplem1  22397  dvcnvrelem2  22419  mdegleb  22464  mdeglt  22465  mdegldg  22466  mdegxrcl  22467  mdegcl  22469  ig1peu  22572  efifo  22934  dvlog  23032  efopnlem2  23038  efopn  23039  f1otrg  24174  axcontlem10  24276  eupares  24975  eupath2lem3  24979  subgornss  25308  ghsubgolemOLD  25372  htthlem  25834  shsss  26231  imaelshi  26977  pjimai  27095  fimarab  27483  sitgclbn  28285  eulerpartlemgvv  28315  eulerpartlemgf  28318  coinfliprv  28421  ballotlemsima  28454  ballotlemro  28461  erdsze2lem2  28648  mrsubrn  28873  msubrn  28889  nocvxminlem  29450  nocvxmin  29451  nobndlem1  29452  nobndlem2  29453  itg2addnclem2  30067  itg2gt0cn  30070  ftc1anclem7  30096  ftc1anc  30098  tailf  30193  ismtyima  30299  ismtyres  30304  heibor1lem  30305  reheibor  30335  elrfirn  30627  isnacs2  30638  isnacs3  30642  fnwe2lem2  30997  lmhmfgima  31030  limccog  31626  mgmhmima  32490  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37993

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-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

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-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  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