MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imassrn Unicode version

Theorem imassrn 4932
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
StepHypRef Expression
1 simpr 449 . . . 4  |-  ( ( x  e.  B  /\  <.
x ,  y >.  e.  A )  ->  <. x ,  y >.  e.  A
)
21eximi 1574 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
32ss2abi 3166 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
4 dfima3 4922 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
5 dfrn3 4776 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
63, 4, 53sstr4i 3138 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1537    e. wcel 1621   {cab 2239    C_ wss 3078   <.cop 3547   ran crn 4581   "cima 4583
This theorem is referenced by:  imaexg  4933  0ima  4938  cnvimass  4940  fimacnv  5509  isofrlem  5689  isofr2  5693  f1oweALT  5703  f1opw2  5923  frxp  6077  smores2  6257  ecss  6587  f1imaen2g  6807  domunsncan  6847  fopwdom  6855  sbthlem2  6857  sbthlem3  6858  sbthlem5  6860  sbthlem6  6861  ssenen  6920  ssfi  6968  fiint  7018  f1opwfi  7043  fissuni  7044  fipreima  7045  marypha1lem  7070  unxpwdom2  7186  tz9.12lem1  7343  acndom2  7565  dfac12lem2  7654  isf34lem5  7888  isf34lem7  7889  isf34lem6  7890  enfin1ai  7894  hsmexlem4  7939  hsmexlem5  7940  fpwwe2lem6  8137  fpwwe2lem9  8140  tskuni  8285  limsupgle  11828  limsupval2  11831  limsupgre  11832  isercolllem2  12016  isercoll  12018  unbenlem  12829  imasless  13316  isacs1i  13403  isacs4lem  14115  mhmima  14275  cntzmhm  14649  gsumzaddlem  15038  dmdprdd  15072  dprdfeq0  15092  dprdres  15098  dprdss  15099  dprdz  15100  subgdmdprd  15104  dprd2dlem1  15111  dprd2da  15112  dmdprdsplit2lem  15115  lmhmlsp  15641  cnclsi  16833  cnprest2  16850  paste  16854  cmpfi  16967  conima  16983  1stcfb  17003  1stckgenlem  17080  kgencn3  17085  xkoco1cn  17183  xkoco2cn  17184  xkococnlem  17185  qtopval2  17219  basqtop  17234  imastopn  17243  kqopn  17257  kqcld  17258  hmeontr  17292  hmeores  17294  hmphdis  17319  cmphaushmeo  17323  qtopf1  17339  fbasrn  17411  uzfbas  17425  elfm  17474  elfm3  17477  imaelfm  17478  rnelfm  17480  tgpconcomp  17627  divstgpopn  17634  tsmsf1o  17659  qtopbaslem  18099  tgqioo  18138  cnheiborlem  18284  bndth  18288  fmcfil  18530  ovoliunlem1  18693  volsup  18745  uniioombllem4  18773  uniioombllem5  18774  opnmblALT  18790  volsup2  18792  mbfimaopnlem  18842  mbflimsup  18853  itg2gt0  18947  c1liplem1  19175  dvcnvrelem2  19197  mdegleb  19282  mdeglt  19283  mdegldg  19284  mdegxrcl  19285  mdegcl  19287  ig1peu  19389  efifo  19741  dvlog  19830  efopnlem2  19836  efopn  19837  subgornss  20803  ghsubgolem  20867  htthlem  21327  shsss  21722  imaelshi  22468  pjimai  22586  erdsze2lem2  22906  eupares  23070  eupath2lem3  23074  nocvxminlem  23512  nocvxmin  23513  axfelem1  23514  axfelem2  23515  axcontlem10  23775  cmptdst  24734  limptlimpr2lem2  24741  supbrr  24802  tailf  25490  ismtyima  25693  ismtyres  25698  heibor1lem  25699  reheibor  25729  funsnfsup  25928  elrfirn  25936  isnacs2  25947  isnacs3  25951  fnwe2lem2  26314  lmhmfgima  26348  frlmsslsp  26414  lindff1  26456  lindfrn  26457  f1lindf  26458  lindfmm  26463  lsslindf  26466  f1omvdconj  26555  psgnunilem1  26582
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601
  Copyright terms: Public domain W3C validator