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

Theorem imassrn 5175
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 448 . . . 4  |-  ( ( x  e.  B  /\  <.
x ,  y >.  e.  A )  ->  <. x ,  y >.  e.  A
)
21eximi 1582 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
32ss2abi 3375 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
4 dfima3 5165 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
5 dfrn3 5019 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
63, 4, 53sstr4i 3347 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1547    e. wcel 1721   {cab 2390    C_ wss 3280   <.cop 3777   ran crn 4838   "cima 4840
This theorem is referenced by:  imaexg  5176  0ima  5181  cnvimass  5183  fimacnv  5821  isofrlem  6019  isofr2  6023  f1oweALT  6033  f1opw2  6257  frxp  6415  smores2  6575  ecss  6905  f1imaen2g  7127  domunsncan  7167  fopwdom  7175  sbthlem2  7177  sbthlem3  7178  sbthlem5  7180  sbthlem6  7181  ssenen  7240  ssfi  7288  fiint  7342  f1opwfi  7368  fissuni  7369  fipreima  7370  marypha1lem  7396  unxpwdom2  7512  tz9.12lem1  7669  acndom2  7891  dfac12lem2  7980  isf34lem5  8214  isf34lem7  8215  isf34lem6  8216  enfin1ai  8220  hsmexlem4  8265  hsmexlem5  8266  fpwwe2lem6  8466  fpwwe2lem9  8469  tskuni  8614  limsupgle  12226  limsupval2  12229  limsupgre  12230  isercolllem2  12414  isercoll  12416  unbenlem  13231  imasless  13720  isacs1i  13837  isacs4lem  14549  mhmima  14718  cntzmhm  15092  gsumzaddlem  15481  dmdprdd  15515  dprdfeq0  15535  dprdres  15541  dprdss  15542  dprdz  15543  subgdmdprd  15547  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2lem  15558  lmhmlsp  16080  cnclsi  17290  cnprest2  17308  paste  17312  cmpfi  17425  conima  17441  1stcfb  17461  1stckgenlem  17538  kgencn3  17543  xkoco1cn  17642  xkoco2cn  17643  xkococnlem  17644  qtopval2  17681  basqtop  17696  imastopn  17705  kqopn  17719  kqcld  17720  hmeontr  17754  hmeores  17756  hmphdis  17781  cmphaushmeo  17785  qtopf1  17801  fbasrn  17869  uzfbas  17883  elfm  17932  elfm3  17935  imaelfm  17936  rnelfm  17938  cnextcn  18051  tgpconcomp  18095  divstgpopn  18102  tsmsf1o  18127  ustimasn  18211  utopbas  18218  restutop  18220  qtopbaslem  18745  tgqioo  18784  cnheiborlem  18932  bndth  18936  fmcfil  19178  ovoliunlem1  19351  volsup  19403  uniioombllem4  19431  uniioombllem5  19432  opnmblALT  19448  volsup2  19450  mbfimaopnlem  19500  mbflimsup  19511  itg2gt0  19605  c1liplem1  19833  dvcnvrelem2  19855  mdegleb  19940  mdeglt  19941  mdegldg  19942  mdegxrcl  19943  mdegcl  19945  ig1peu  20047  efifo  20402  dvlog  20495  efopnlem2  20501  efopn  20502  eupares  21650  eupath2lem3  21654  subgornss  21847  ghsubgolem  21911  htthlem  22373  shsss  22768  imaelshi  23514  pjimai  23632  sitgclbn  24610  coinfliprv  24693  ballotlemsima  24726  ballotlemro  24733  erdsze2lem2  24843  nocvxminlem  25558  nocvxmin  25559  nobndlem1  25560  nobndlem2  25561  axcontlem10  25816  itg2addnclem2  26156  itg2gt0cn  26159  tailf  26294  ismtyima  26402  ismtyres  26407  heibor1lem  26408  reheibor  26438  funsnfsup  26633  elrfirn  26639  isnacs2  26650  isnacs3  26654  fnwe2lem2  27016  lmhmfgima  27050  frlmsslsp  27116  lindff1  27158  lindfrn  27159  f1lindf  27160  lindfmm  27165  lsslindf  27168  f1omvdconj  27257  psgnunilem1  27284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-cnv 4845  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850
  Copyright terms: Public domain W3C validator