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

Theorem imassrn 5201
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 exsimpr 1645 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
21ss2abi 3445 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
3 dfima3 5193 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
4 dfrn3 5050 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
52, 3, 43sstr4i 3416 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   E.wex 1586    e. wcel 1756   {cab 2429    C_ wss 3349   <.cop 3904   ran crn 4862   "cima 4864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-opab 4372  df-xp 4867  df-cnv 4869  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874
This theorem is referenced by:  0ima  5206  cnvimass  5210  fimacnv  5856  isofrlem  6052  isofr2  6056  f1opw2  6334  imaexg  6536  f1oweALT  6582  frxp  6703  smores2  6836  ecss  7163  f1imaen2g  7391  domunsncan  7432  fopwdom  7440  sbthlem2  7443  sbthlem3  7444  sbthlem5  7446  sbthlem6  7447  ssenen  7506  ssfi  7554  fiint  7609  f1opwfi  7636  fissuni  7637  fipreima  7638  marypha1lem  7704  unxpwdom2  7824  tz9.12lem1  8015  acndom2  8245  dfac12lem2  8334  isf34lem5  8568  isf34lem7  8569  isf34lem6  8570  enfin1ai  8574  hsmexlem4  8619  hsmexlem5  8620  fpwwe2lem6  8823  fpwwe2lem9  8826  tskuni  8971  limsupgle  12976  limsupval2  12979  limsupgre  12980  isercolllem2  13164  isercoll  13166  unbenlem  13990  imasless  14499  isacs1i  14616  isacs4lem  15359  mhmima  15512  cntzmhm  15877  f1omvdconj  15973  psgnunilem1  16020  gsumzaddlem  16429  gsumzaddlemOLD  16431  dmdprdd  16503  dprdfeq0  16534  dprdfeq0OLD  16541  dprdres  16547  dprdss  16548  dprdz  16549  subgdmdprd  16553  dprd2dlem1  16562  dprd2da  16563  dmdprdsplit2lem  16566  lmhmlsp  17152  funsnfsupOLD  17692  frlmsslsp  18245  frlmsslspOLD  18246  lindff1  18271  lindfrn  18272  f1lindf  18273  lindfmm  18278  lsslindf  18281  cnclsi  18898  cnprest2  18916  paste  18920  cmpfi  19033  conima  19051  1stcfb  19071  1stckgenlem  19148  kgencn3  19153  xkoco1cn  19252  xkoco2cn  19253  xkococnlem  19254  qtopval2  19291  basqtop  19306  imastopn  19315  kqopn  19329  kqcld  19330  hmeontr  19364  hmeores  19366  hmphdis  19391  cmphaushmeo  19395  qtopf1  19411  fbasrn  19479  uzfbas  19493  elfm  19542  elfm3  19545  imaelfm  19546  rnelfm  19548  cnextcn  19661  tgpconcomp  19705  divstgpopn  19712  tsmsf1o  19741  ustimasn  19825  utopbas  19832  restutop  19834  qtopbaslem  20359  tgqioo  20399  cnheiborlem  20548  bndth  20552  fmcfil  20805  ovoliunlem1  21007  volsup  21059  uniioombllem4  21088  uniioombllem5  21089  opnmblALT  21105  volsup2  21107  mbfimaopnlem  21155  mbflimsup  21166  itg2gt0  21260  c1liplem1  21490  dvcnvrelem2  21512  mdegleb  21557  mdeglt  21558  mdegldg  21559  mdegxrcl  21560  mdegcl  21562  ig1peu  21665  efifo  22025  dvlog  22118  efopnlem2  22124  efopn  22125  f1otrg  23139  axcontlem10  23241  eupares  23618  eupath2lem3  23622  subgornss  23815  ghsubgolem  23879  htthlem  24341  shsss  24738  imaelshi  25484  pjimai  25602  gsummpt2co  26271  sitgclbn  26751  eulerpartlemgvv  26781  eulerpartlemgf  26784  coinfliprv  26887  ballotlemsima  26920  ballotlemro  26927  erdsze2lem2  27114  nocvxminlem  27853  nocvxmin  27854  nobndlem1  27855  nobndlem2  27856  itg2addnclem2  28470  itg2gt0cn  28473  ftc1anclem7  28499  ftc1anc  28501  tailf  28622  ismtyima  28728  ismtyres  28733  heibor1lem  28734  reheibor  28764  elrfirn  29057  isnacs2  29068  isnacs3  29072  fnwe2lem2  29430  lmhmfgima  29463
  Copyright terms: Public domain W3C validator