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

Theorem imassrn 5185
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 1738 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
21ss2abi 3487 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
3 dfima3 5177 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
4 dfrn3 5029 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
52, 3, 43sstr4i 3457 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 376   E.wex 1671    e. wcel 1904   {cab 2457    C_ wss 3390   <.cop 3965   ran crn 4840   "cima 4842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-xp 4845  df-cnv 4847  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852
This theorem is referenced by:  0ima  5190  cnvimass  5194  fimass  5772  fimacnv  6027  isofrlem  6249  isofr2  6253  f1opw2  6541  imaexg  6749  f1oweALT  6796  frxp  6925  smores2  7091  ecss  7423  f1imaen2g  7648  domunsncan  7690  fopwdom  7698  sbthlem2  7701  sbthlem3  7702  sbthlem5  7704  sbthlem6  7705  ssenen  7764  ssfi  7810  fiint  7866  f1opwfi  7896  fissuni  7897  fipreima  7898  marypha1lem  7965  unxpwdom2  8121  tz9.12lem1  8276  acndom2  8503  dfac12lem2  8592  isf34lem5  8826  isf34lem7  8827  isf34lem6  8828  enfin1ai  8832  hsmexlem4  8877  hsmexlem5  8878  fpwwe2lem6  9078  fpwwe2lem9  9081  tskuni  9226  limsupgle  13612  limsupval2  13617  limsupval2OLD  13618  limsupgre  13619  limsupgreOLD  13620  isercolllem2  13806  isercoll  13808  unbenlem  14931  imasless  15524  isacs1i  15641  isacs4lem  16492  mhmima  16688  cntzmhm  17070  f1omvdconj  17165  psgnunilem1  17212  gsumzaddlem  17632  dmdprdd  17709  dprdfeq0  17733  dprdres  17739  dprdss  17740  dprdz  17741  subgdmdprd  17745  dprd2dlem1  17752  dprd2da  17753  dmdprdsplit2lem  17756  lmhmlsp  18350  frlmsslsp  19431  lindff1  19455  lindfrn  19456  f1lindf  19457  lindfmm  19462  lsslindf  19465  cnclsi  20365  cnprest2  20383  paste  20387  cmpfi  20500  conima  20517  1stcfb  20537  1stckgenlem  20645  kgencn3  20650  xkoco1cn  20749  xkoco2cn  20750  xkococnlem  20751  qtopval2  20788  basqtop  20803  imastopn  20812  kqopn  20826  kqcld  20827  hmeontr  20861  hmeores  20863  hmphdis  20888  cmphaushmeo  20892  qtopf1  20908  fbasrn  20977  uzfbas  20991  elfm  21040  elfm3  21043  imaelfm  21044  rnelfm  21046  cnextcn  21160  tgpconcomp  21205  qustgpopn  21212  tsmsf1o  21237  ustimasn  21321  utopbas  21328  restutop  21330  qtopbaslem  21857  tgqioo  21896  cnheiborlem  22060  bndth  22064  fmcfil  22320  ovoliunlem1  22533  volsup  22588  uniioombllem4  22623  uniioombllem5  22624  opnmblALT  22640  volsup2  22642  mbfimaopnlem  22690  mbflimsup  22702  mbflimsupOLD  22703  itg2gt0  22797  c1liplem1  23027  dvcnvrelem2  23049  mdegleb  23092  mdeglt  23093  mdegldg  23094  mdegxrcl  23095  mdegcl  23097  ig1peu  23201  ig1peuOLD  23202  efifo  23575  dvlog  23675  efopnlem2  23681  efopn  23682  f1otrg  24980  axcontlem10  25082  eupares  25782  eupath2lem3  25786  subgornss  26115  ghsubgolemOLD  26179  htthlem  26651  shsss  27047  imaelshi  27792  pjimai  27910  fimarab  28320  gsummpt2co  28617  sitgclbn  29249  sitgaddlemb  29254  eulerpartlemgvv  29282  eulerpartlemgf  29285  coinfliprv  29388  ballotlemsima  29421  ballotlemro  29428  ballotlemsimaOLD  29459  ballotlemroOLD  29466  erdsze2lem2  29999  mrsubrn  30223  msubrn  30239  nocvxminlem  30650  nocvxmin  30651  nobndlem1  30652  nobndlem2  30653  tailf  31102  dissneqlem  31812  poimirlem1  32005  poimirlem2  32006  poimirlem3  32007  poimirlem11  32015  poimirlem12  32016  poimirlem15  32019  poimirlem16  32020  poimirlem19  32023  poimirlem30  32034  itg2addnclem2  32058  itg2gt0cn  32061  ftc1anclem7  32087  ftc1anc  32089  ismtyima  32199  ismtyres  32204  heibor1lem  32205  reheibor  32235  elrfirn  35608  isnacs2  35619  isnacs3  35623  fnwe2lem2  35980  lmhmfgima  36013  brtrclfv2  36390  xphe  36447  imo72b2lem0  36679  imo72b2lem2  36681  imo72b2lem1  36685  imo72b2  36689  limccog  37797  mgmhmima  40310
  Copyright terms: Public domain W3C validator