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

Theorem imassrn 5168
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 3412 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
3 dfima3 5160 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
4 dfrn3 5016 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
52, 3, 43sstr4i 3383 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   E.wex 1589    e. wcel 1755   {cab 2419    C_ wss 3316   <.cop 3871   ran crn 4828   "cima 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-xp 4833  df-cnv 4835  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840
This theorem is referenced by:  0ima  5173  cnvimass  5177  fimacnv  5823  isofrlem  6018  isofr2  6022  f1opw2  6302  imaexg  6504  f1oweALT  6550  frxp  6671  smores2  6801  ecss  7130  f1imaen2g  7358  domunsncan  7399  fopwdom  7407  sbthlem2  7410  sbthlem3  7411  sbthlem5  7413  sbthlem6  7414  ssenen  7473  ssfi  7521  fiint  7576  f1opwfi  7603  fissuni  7604  fipreima  7605  marypha1lem  7671  unxpwdom2  7791  tz9.12lem1  7982  acndom2  8212  dfac12lem2  8301  isf34lem5  8535  isf34lem7  8536  isf34lem6  8537  enfin1ai  8541  hsmexlem4  8586  hsmexlem5  8587  fpwwe2lem6  8789  fpwwe2lem9  8792  tskuni  8937  limsupgle  12938  limsupval2  12941  limsupgre  12942  isercolllem2  13126  isercoll  13128  unbenlem  13951  imasless  14460  isacs1i  14577  isacs4lem  15320  mhmima  15472  cntzmhm  15835  f1omvdconj  15931  psgnunilem1  15978  gsumzaddlem  16387  gsumzaddlemOLD  16389  dmdprdd  16454  dprdfeq0  16485  dprdfeq0OLD  16492  dprdres  16498  dprdss  16499  dprdz  16500  subgdmdprd  16504  dprd2dlem1  16513  dprd2da  16514  dmdprdsplit2lem  16517  lmhmlsp  17051  funsnfsupOLD  17568  frlmsslsp  18064  frlmsslspOLD  18065  lindff1  18090  lindfrn  18091  f1lindf  18092  lindfmm  18097  lsslindf  18100  cnclsi  18717  cnprest2  18735  paste  18739  cmpfi  18852  conima  18870  1stcfb  18890  1stckgenlem  18967  kgencn3  18972  xkoco1cn  19071  xkoco2cn  19072  xkococnlem  19073  qtopval2  19110  basqtop  19125  imastopn  19134  kqopn  19148  kqcld  19149  hmeontr  19183  hmeores  19185  hmphdis  19210  cmphaushmeo  19214  qtopf1  19230  fbasrn  19298  uzfbas  19312  elfm  19361  elfm3  19364  imaelfm  19365  rnelfm  19367  cnextcn  19480  tgpconcomp  19524  divstgpopn  19531  tsmsf1o  19560  ustimasn  19644  utopbas  19651  restutop  19653  qtopbaslem  20178  tgqioo  20218  cnheiborlem  20367  bndth  20371  fmcfil  20624  ovoliunlem1  20826  volsup  20878  uniioombllem4  20907  uniioombllem5  20908  opnmblALT  20924  volsup2  20926  mbfimaopnlem  20974  mbflimsup  20985  itg2gt0  21079  c1liplem1  21309  dvcnvrelem2  21331  mdegleb  21419  mdeglt  21420  mdegldg  21421  mdegxrcl  21422  mdegcl  21424  ig1peu  21527  efifo  21887  dvlog  21980  efopnlem2  21986  efopn  21987  f1otrg  22939  axcontlem10  23041  eupares  23418  eupath2lem3  23422  subgornss  23615  ghsubgolem  23679  htthlem  24141  shsss  24538  imaelshi  25284  pjimai  25402  gsummpt2co  26100  sitgclbn  26576  eulerpartlemgvv  26606  eulerpartlemgf  26609  coinfliprv  26712  ballotlemsima  26745  ballotlemro  26752  erdsze2lem2  26939  nocvxminlem  27677  nocvxmin  27678  nobndlem1  27679  nobndlem2  27680  itg2addnclem2  28285  itg2gt0cn  28288  ftc1anclem7  28314  ftc1anc  28316  tailf  28437  ismtyima  28543  ismtyres  28548  heibor1lem  28549  reheibor  28579  elrfirn  28873  isnacs2  28884  isnacs3  28888  fnwe2lem2  29246  lmhmfgima  29279
  Copyright terms: Public domain W3C validator