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

Theorem imassrn 5338
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 1665 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
21ss2abi 3557 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
3 dfima3 5330 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
4 dfrn3 5182 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
52, 3, 43sstr4i 3528 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   E.wex 1599    e. wcel 1804   {cab 2428    C_ wss 3461   <.cop 4020   ran crn 4990   "cima 4992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-cnv 4997  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002
This theorem is referenced by:  0ima  5343  cnvimass  5347  fimacnv  6004  isofrlem  6221  isofr2  6225  f1opw2  6513  imaexg  6722  f1oweALT  6769  frxp  6895  smores2  7027  ecss  7355  f1imaen2g  7578  domunsncan  7619  fopwdom  7627  sbthlem2  7630  sbthlem3  7631  sbthlem5  7633  sbthlem6  7634  ssenen  7693  ssfi  7742  fiint  7799  f1opwfi  7826  fissuni  7827  fipreima  7828  marypha1lem  7895  unxpwdom2  8017  tz9.12lem1  8208  acndom2  8438  dfac12lem2  8527  isf34lem5  8761  isf34lem7  8762  isf34lem6  8763  enfin1ai  8767  hsmexlem4  8812  hsmexlem5  8813  fpwwe2lem6  9016  fpwwe2lem9  9019  tskuni  9164  limsupgle  13281  limsupval2  13284  limsupgre  13285  isercolllem2  13469  isercoll  13471  unbenlem  14407  imasless  14918  isacs1i  15035  isacs4lem  15776  mhmima  15972  cntzmhm  16354  f1omvdconj  16449  psgnunilem1  16496  gsumzaddlem  16912  gsumzaddlemOLD  16914  dmdprdd  17008  dprdfeq0  17040  dprdfeq0OLD  17047  dprdres  17053  dprdss  17054  dprdz  17055  subgdmdprd  17059  dprd2dlem1  17068  dprd2da  17069  dmdprdsplit2lem  17072  lmhmlsp  17673  funsnfsupOLD  18234  frlmsslsp  18806  frlmsslspOLD  18807  lindff1  18832  lindfrn  18833  f1lindf  18834  lindfmm  18839  lsslindf  18842  cnclsi  19750  cnprest2  19768  paste  19772  cmpfi  19885  conima  19903  1stcfb  19923  1stckgenlem  20031  kgencn3  20036  xkoco1cn  20135  xkoco2cn  20136  xkococnlem  20137  qtopval2  20174  basqtop  20189  imastopn  20198  kqopn  20212  kqcld  20213  hmeontr  20247  hmeores  20249  hmphdis  20274  cmphaushmeo  20278  qtopf1  20294  fbasrn  20362  uzfbas  20376  elfm  20425  elfm3  20428  imaelfm  20429  rnelfm  20431  cnextcn  20544  tgpconcomp  20588  qustgpopn  20595  tsmsf1o  20624  ustimasn  20708  utopbas  20715  restutop  20717  qtopbaslem  21242  tgqioo  21282  cnheiborlem  21431  bndth  21435  fmcfil  21688  ovoliunlem1  21890  volsup  21943  uniioombllem4  21972  uniioombllem5  21973  opnmblALT  21989  volsup2  21991  mbfimaopnlem  22039  mbflimsup  22050  itg2gt0  22144  c1liplem1  22374  dvcnvrelem2  22396  mdegleb  22441  mdeglt  22442  mdegldg  22443  mdegxrcl  22444  mdegcl  22446  ig1peu  22549  efifo  22910  dvlog  23008  efopnlem2  23014  efopn  23015  f1otrg  24150  axcontlem10  24252  eupares  24951  eupath2lem3  24955  subgornss  25284  ghsubgolemOLD  25348  htthlem  25810  shsss  26207  imaelshi  26953  pjimai  27071  fimarab  27459  sitgclbn  28262  eulerpartlemgvv  28292  eulerpartlemgf  28295  coinfliprv  28398  ballotlemsima  28431  ballotlemro  28438  erdsze2lem2  28625  mrsubrn  28850  msubrn  28866  nocvxminlem  29425  nocvxmin  29426  nobndlem1  29427  nobndlem2  29428  itg2addnclem2  30042  itg2gt0cn  30045  ftc1anclem7  30071  ftc1anc  30073  tailf  30168  ismtyima  30274  ismtyres  30279  heibor1lem  30280  reheibor  30310  elrfirn  30602  isnacs2  30613  isnacs3  30617  fnwe2lem2  30972  lmhmfgima  31005  limccog  31534  mgmhmima  32328  imo72b2lem0  37651  imo72b2lem2  37653  imo72b2lem1  37657  imo72b2  37662
  Copyright terms: Public domain W3C validator