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

Theorem imassrn 5025
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.
StepHypRef Expression
1 simpr 447 . . . 4  |-  ( ( x  e.  B  /\  <.
x ,  y >.  e.  A )  ->  <. x ,  y >.  e.  A
)
21eximi 1563 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
32ss2abi 3245 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
4 dfima3 5015 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
5 dfrn3 4869 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
63, 4, 53sstr4i 3217 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1528    e. wcel 1684   {cab 2269    C_ wss 3152   <.cop 3643   ran crn 4690   "cima 4692
This theorem is referenced by:  imaexg  5026  0ima  5031  cnvimass  5033  fimacnv  5657  isofrlem  5837  isofr2  5841  f1oweALT  5851  f1opw2  6071  frxp  6225  smores2  6371  ecss  6701  f1imaen2g  6922  domunsncan  6962  fopwdom  6970  sbthlem2  6972  sbthlem3  6973  sbthlem5  6975  sbthlem6  6976  ssenen  7035  ssfi  7083  fiint  7133  f1opwfi  7159  fissuni  7160  fipreima  7161  marypha1lem  7186  unxpwdom2  7302  tz9.12lem1  7459  acndom2  7681  dfac12lem2  7770  isf34lem5  8004  isf34lem7  8005  isf34lem6  8006  enfin1ai  8010  hsmexlem4  8055  hsmexlem5  8056  fpwwe2lem6  8257  fpwwe2lem9  8260  tskuni  8405  limsupgle  11951  limsupval2  11954  limsupgre  11955  isercolllem2  12139  isercoll  12141  unbenlem  12955  imasless  13442  isacs1i  13559  isacs4lem  14271  mhmima  14440  cntzmhm  14814  gsumzaddlem  15203  dmdprdd  15237  dprdfeq0  15257  dprdres  15263  dprdss  15264  dprdz  15265  subgdmdprd  15269  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2lem  15280  lmhmlsp  15806  cnclsi  17001  cnprest2  17018  paste  17022  cmpfi  17135  conima  17151  1stcfb  17171  1stckgenlem  17248  kgencn3  17253  xkoco1cn  17351  xkoco2cn  17352  xkococnlem  17353  qtopval2  17387  basqtop  17402  imastopn  17411  kqopn  17425  kqcld  17426  hmeontr  17460  hmeores  17462  hmphdis  17487  cmphaushmeo  17491  qtopf1  17507  fbasrn  17579  uzfbas  17593  elfm  17642  elfm3  17645  imaelfm  17646  rnelfm  17648  tgpconcomp  17795  divstgpopn  17802  tsmsf1o  17827  qtopbaslem  18267  tgqioo  18306  cnheiborlem  18452  bndth  18456  fmcfil  18698  ovoliunlem1  18861  volsup  18913  uniioombllem4  18941  uniioombllem5  18942  opnmblALT  18958  volsup2  18960  mbfimaopnlem  19010  mbflimsup  19021  itg2gt0  19115  c1liplem1  19343  dvcnvrelem2  19365  mdegleb  19450  mdeglt  19451  mdegldg  19452  mdegxrcl  19453  mdegcl  19455  ig1peu  19557  efifo  19909  dvlog  19998  efopnlem2  20004  efopn  20005  subgornss  20973  ghsubgolem  21037  htthlem  21497  shsss  21892  imaelshi  22638  pjimai  22756  ballotlemsima  23074  ballotlemro  23081  coinfliprv  23683  erdsze2lem2  23735  eupares  23899  eupath2lem3  23903  nocvxminlem  24344  nocvxmin  24345  nobndlem1  24346  nobndlem2  24347  axcontlem10  24601  cmptdst  25568  limptlimpr2lem2  25575  supbrr  25636  tailf  26324  ismtyima  26527  ismtyres  26532  heibor1lem  26533  reheibor  26563  funsnfsup  26762  elrfirn  26770  isnacs2  26781  isnacs3  26785  fnwe2lem2  27148  lmhmfgima  27182  frlmsslsp  27248  lindff1  27290  lindfrn  27291  f1lindf  27292  lindfmm  27297  lsslindf  27300  f1omvdconj  27389  psgnunilem1  27416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702
  Copyright terms: Public domain W3C validator