Theorem imassrn 5477

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	|- ( A " B ) C_ ran A

Proof of Theorem imassrn

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

Step	Hyp	Ref	Expression
1		exsimpr 1796	. . 3 |- ( E. x ( x e. B /\ <. x , y >. e. A ) -> E. x <. x , y >. e. A )
2	1	ss2abi 3674	. 2 |- { y | E. x ( x e. B /\ <. x , y >. e. A ) } C_ { y | E. x <. x , y >. e. A }
3		dfima3 5469	. 2 |- ( A " B ) = { y | E. x ( x e. B /\ <. x , y >. e. A ) }
4		dfrn3 5312	. 2 |- ran A = { y | E. x <. x , y >. e. A }
5	2, 3, 4	3sstr4i 3644	1 |- ( A " B ) C_ ran A

Syntax hints:   /\ wa 384   E.wex 1704   e. wcel 1990   {cab 2608   C_ wss 3574   <.cop 4183   ran crn 5115   "cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  0ima  5482  cnvimass  5485  fimass  6081  fimacnv  6347  isofrlem  6590  isofr2  6594  f1opw2  6888  imaexg  7103  f1oweALT  7152  frxp  7287  smores2  7451  ecss  7788  f1imaen2g  8017  domunsncan  8060  fopwdom  8068  sbthlem2  8071  sbthlem3  8072  sbthlem5  8074  sbthlem6  8075  ssenen  8134  ssfi  8180  fiint  8237  f1opwfi  8270  marypha1lem  8339  unxpwdom2  8493  tz9.12lem1  8650  acndom2  8877  dfac12lem2  8966  isf34lem5  9200  isf34lem7  9201  isf34lem6  9202  enfin1ai  9206  hsmexlem4  9251  hsmexlem5  9252  fpwwe2lem6  9457  fpwwe2lem9  9460  tskuni  9605  limsupgle  14208  limsupval2  14211  limsupgre  14212  isercolllem2  14396  isercoll  14398  unbenlem  15612  imasless  16200  isacs1i  16318  isacs4lem  17168  mhmima  17363  cntzmhm  17771  f1omvdconj  17866  psgnunilem1  17913  gsumzaddlem  18321  dmdprdd  18398  dprdfeq0  18421  dprdres  18427  dprdss  18428  dprdz  18429  subgdmdprd  18433  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2lem  18444  lmhmlsp  19049  frlmsslsp  20135  lindff1  20159  lindfrn  20160  f1lindf  20161  lindfmm  20166  lsslindf  20169  cnclsi  21076  cnprest2  21094  paste  21098  cmpfi  21211  connima  21228  1stcfb  21248  1stckgenlem  21356  kgencn3  21361  xkoco1cn  21460  xkoco2cn  21461  xkococnlem  21462  qtopval2  21499  basqtop  21514  imastopn  21523  kqopn  21537  kqcld  21538  hmeontr  21572  hmeores  21574  hmphdis  21599  cmphaushmeo  21603  qtopf1  21619  fbasrn  21688  uzfbas  21702  elfm  21751  elfm3  21754  imaelfm  21755  rnelfm  21757  cnextcn  21871  tgpconncomp  21916  qustgpopn  21923  tsmsf1o  21948  ustimasn  22032  utopbas  22039  restutop  22041  qtopbaslem  22562  tgqioo  22603  cnheiborlem  22753  bndth  22757  fmcfil  23070  ovoliunlem1  23270  volsup  23324  uniioombllem4  23354  uniioombllem5  23355  opnmblALT  23371  volsup2  23373  mbfimaopnlem  23422  mbflimsup  23433  itg2gt0  23527  c1liplem1  23759  dvcnvrelem2  23781  mdegleb  23824  mdeglt  23825  mdegldg  23826  mdegxrcl  23827  mdegcl  23829  ig1peu  23931  efifo  24293  dvlog  24397  efopnlem2  24403  efopn  24404  f1otrg  25751  axcontlem10  25853  htthlem  27774  shsss  28172  imaelshi  28917  pjimai  29035  fimarab  29445  gsummpt2co  29780  sitgclbn  30405  sitgaddlemb  30410  eulerpartlemgvv  30438  eulerpartlemgf  30441  coinfliprv  30544  ballotlemsima  30577  ballotlemro  30584  erdsze2lem2  31186  mrsubrn  31410  msubrn  31426  bdayimaon  31843  nosupbday  31851  noetalem3  31865  noetalem4  31866  nocvxminlem  31893  nocvxmin  31894  tailf  32370  dissneqlem  33187  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem19  33428  poimirlem30  33439  itg2addnclem2  33462  itg2gt0cn  33465  ftc1anclem7  33491  ftc1anc  33493  ismtyima  33602  ismtyres  33607  heibor1lem  33608  reheibor  33638  elrfirn  37258  isnacs2  37269  isnacs3  37273  fnwe2lem2  37621  lmhmfgima  37654  brtrclfv2  38019  xphe  38075  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  limccog  39852  liminfval2  40000  mgmhmima  41802