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

Theorem imassrn 5207
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 1585 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
32ss2abi 3407 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
4 dfima3 5197 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
5 dfrn3 5051 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
63, 4, 53sstr4i 3379 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1550    e. wcel 1725   {cab 2421    C_ wss 3312   <.cop 3809   ran crn 4870   "cima 4872
This theorem is referenced by:  imaexg  5208  0ima  5213  cnvimass  5215  fimacnv  5853  isofrlem  6051  isofr2  6055  f1oweALT  6065  f1opw2  6289  frxp  6447  smores2  6607  ecss  6937  f1imaen2g  7159  domunsncan  7199  fopwdom  7207  sbthlem2  7209  sbthlem3  7210  sbthlem5  7212  sbthlem6  7213  ssenen  7272  ssfi  7320  fiint  7374  f1opwfi  7401  fissuni  7402  fipreima  7403  marypha1lem  7429  unxpwdom2  7545  tz9.12lem1  7702  acndom2  7924  dfac12lem2  8013  isf34lem5  8247  isf34lem7  8248  isf34lem6  8249  enfin1ai  8253  hsmexlem4  8298  hsmexlem5  8299  fpwwe2lem6  8499  fpwwe2lem9  8502  tskuni  8647  limsupgle  12259  limsupval2  12262  limsupgre  12263  isercolllem2  12447  isercoll  12449  unbenlem  13264  imasless  13753  isacs1i  13870  isacs4lem  14582  mhmima  14751  cntzmhm  15125  gsumzaddlem  15514  dmdprdd  15548  dprdfeq0  15568  dprdres  15574  dprdss  15575  dprdz  15576  subgdmdprd  15580  dprd2dlem1  15587  dprd2da  15588  dmdprdsplit2lem  15591  lmhmlsp  16113  cnclsi  17324  cnprest2  17342  paste  17346  cmpfi  17459  conima  17476  1stcfb  17496  1stckgenlem  17573  kgencn3  17578  xkoco1cn  17677  xkoco2cn  17678  xkococnlem  17679  qtopval2  17716  basqtop  17731  imastopn  17740  kqopn  17754  kqcld  17755  hmeontr  17789  hmeores  17791  hmphdis  17816  cmphaushmeo  17820  qtopf1  17836  fbasrn  17904  uzfbas  17918  elfm  17967  elfm3  17970  imaelfm  17971  rnelfm  17973  cnextcn  18086  tgpconcomp  18130  divstgpopn  18137  tsmsf1o  18162  ustimasn  18246  utopbas  18253  restutop  18255  qtopbaslem  18780  tgqioo  18819  cnheiborlem  18967  bndth  18971  fmcfil  19213  ovoliunlem1  19386  volsup  19438  uniioombllem4  19466  uniioombllem5  19467  opnmblALT  19483  volsup2  19485  mbfimaopnlem  19535  mbflimsup  19546  itg2gt0  19640  c1liplem1  19868  dvcnvrelem2  19890  mdegleb  19975  mdeglt  19976  mdegldg  19977  mdegxrcl  19978  mdegcl  19980  ig1peu  20082  efifo  20437  dvlog  20530  efopnlem2  20536  efopn  20537  eupares  21685  eupath2lem3  21689  subgornss  21882  ghsubgolem  21946  htthlem  22408  shsss  22803  imaelshi  23549  pjimai  23667  sitgclbn  24645  coinfliprv  24728  ballotlemsima  24761  ballotlemro  24768  erdsze2lem2  24878  nocvxminlem  25599  nocvxmin  25600  nobndlem1  25601  nobndlem2  25602  axcontlem10  25860  itg2addnclem2  26203  itg2gt0cn  26206  tailf  26341  ismtyima  26449  ismtyres  26454  heibor1lem  26455  reheibor  26485  funsnfsup  26680  elrfirn  26686  isnacs2  26697  isnacs3  26701  fnwe2lem2  27063  lmhmfgima  27097  frlmsslsp  27163  lindff1  27205  lindfrn  27206  f1lindf  27207  lindfmm  27212  lsslindf  27215  f1omvdconj  27304  psgnunilem1  27331
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-xp 4875  df-cnv 4877  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882
  Copyright terms: Public domain W3C validator