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

Theorem imassrn 5336
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 1683 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
21ss2abi 3558 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
3 dfima3 5328 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
4 dfrn3 5181 . 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 367   E.wex 1617    e. wcel 1823   {cab 2439    C_ wss 3461   <.cop 4022   ran crn 4989   "cima 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-xp 4994  df-cnv 4996  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001
This theorem is referenced by:  0ima  5341  cnvimass  5345  fimacnv  5995  isofrlem  6211  isofr2  6215  f1opw2  6501  imaexg  6710  f1oweALT  6757  frxp  6883  smores2  7017  ecss  7345  f1imaen2g  7569  domunsncan  7610  fopwdom  7618  sbthlem2  7621  sbthlem3  7622  sbthlem5  7624  sbthlem6  7625  ssenen  7684  ssfi  7733  fiint  7789  f1opwfi  7816  fissuni  7817  fipreima  7818  marypha1lem  7885  unxpwdom2  8006  tz9.12lem1  8196  acndom2  8426  dfac12lem2  8515  isf34lem5  8749  isf34lem7  8750  isf34lem6  8751  enfin1ai  8755  hsmexlem4  8800  hsmexlem5  8801  fpwwe2lem6  9002  fpwwe2lem9  9005  tskuni  9150  limsupgle  13385  limsupval2  13388  limsupgre  13389  isercolllem2  13573  isercoll  13575  unbenlem  14513  imasless  15032  isacs1i  15149  isacs4lem  16000  mhmima  16196  cntzmhm  16578  f1omvdconj  16673  psgnunilem1  16720  gsumzaddlem  17136  gsumzaddlemOLD  17138  dmdprdd  17228  dprdfeq0  17260  dprdfeq0OLD  17267  dprdres  17273  dprdss  17274  dprdz  17275  subgdmdprd  17279  dprd2dlem1  17288  dprd2da  17289  dmdprdsplit2lem  17292  lmhmlsp  17893  funsnfsupOLD  18454  frlmsslsp  19001  lindff1  19025  lindfrn  19026  f1lindf  19027  lindfmm  19032  lsslindf  19035  cnclsi  19943  cnprest2  19961  paste  19965  cmpfi  20078  conima  20095  1stcfb  20115  1stckgenlem  20223  kgencn3  20228  xkoco1cn  20327  xkoco2cn  20328  xkococnlem  20329  qtopval2  20366  basqtop  20381  imastopn  20390  kqopn  20404  kqcld  20405  hmeontr  20439  hmeores  20441  hmphdis  20466  cmphaushmeo  20470  qtopf1  20486  fbasrn  20554  uzfbas  20568  elfm  20617  elfm3  20620  imaelfm  20621  rnelfm  20623  cnextcn  20736  tgpconcomp  20780  qustgpopn  20787  tsmsf1o  20816  ustimasn  20900  utopbas  20907  restutop  20909  qtopbaslem  21434  tgqioo  21474  cnheiborlem  21623  bndth  21627  fmcfil  21880  ovoliunlem1  22082  volsup  22135  uniioombllem4  22164  uniioombllem5  22165  opnmblALT  22181  volsup2  22183  mbfimaopnlem  22231  mbflimsup  22242  itg2gt0  22336  c1liplem1  22566  dvcnvrelem2  22588  mdegleb  22633  mdeglt  22634  mdegldg  22635  mdegxrcl  22636  mdegcl  22638  ig1peu  22741  efifo  23103  dvlog  23203  efopnlem2  23209  efopn  23210  f1otrg  24379  axcontlem10  24481  eupares  25180  eupath2lem3  25184  subgornss  25509  ghsubgolemOLD  25573  htthlem  26035  shsss  26432  imaelshi  27178  pjimai  27296  fimarab  27707  gsummpt2co  28008  sitgclbn  28552  eulerpartlemgvv  28582  eulerpartlemgf  28585  coinfliprv  28688  ballotlemsima  28721  ballotlemro  28728  erdsze2lem2  28915  mrsubrn  29140  msubrn  29156  nocvxminlem  29693  nocvxmin  29694  nobndlem1  29695  nobndlem2  29696  itg2addnclem2  30310  itg2gt0cn  30313  ftc1anclem7  30339  ftc1anc  30341  tailf  30436  ismtyima  30542  ismtyres  30547  heibor1lem  30548  reheibor  30578  elrfirn  30870  isnacs2  30881  isnacs3  30885  fnwe2lem2  31239  lmhmfgima  31272  limccog  31868  mgmhmima  32881  brtrclfv2  38261  imo72b2lem0  38495  imo72b2lem2  38497  imo72b2lem1  38501  imo72b2  38506
  Copyright terms: Public domain W3C validator