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

Theorem imassrn 5041
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 447 . . . 4  |-  ( ( x  e.  B  /\  <.
x ,  y >.  e.  A )  ->  <. x ,  y >.  e.  A
)
21eximi 1566 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
32ss2abi 3258 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
4 dfima3 5031 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
5 dfrn3 4885 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
63, 4, 53sstr4i 3230 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1531    e. wcel 1696   {cab 2282    C_ wss 3165   <.cop 3656   ran crn 4706   "cima 4708
This theorem is referenced by:  imaexg  5042  0ima  5047  cnvimass  5049  fimacnv  5673  isofrlem  5853  isofr2  5857  f1oweALT  5867  f1opw2  6087  frxp  6241  smores2  6387  ecss  6717  f1imaen2g  6938  domunsncan  6978  fopwdom  6986  sbthlem2  6988  sbthlem3  6989  sbthlem5  6991  sbthlem6  6992  ssenen  7051  ssfi  7099  fiint  7149  f1opwfi  7175  fissuni  7176  fipreima  7177  marypha1lem  7202  unxpwdom2  7318  tz9.12lem1  7475  acndom2  7697  dfac12lem2  7786  isf34lem5  8020  isf34lem7  8021  isf34lem6  8022  enfin1ai  8026  hsmexlem4  8071  hsmexlem5  8072  fpwwe2lem6  8273  fpwwe2lem9  8276  tskuni  8421  limsupgle  11967  limsupval2  11970  limsupgre  11971  isercolllem2  12155  isercoll  12157  unbenlem  12971  imasless  13458  isacs1i  13575  isacs4lem  14287  mhmima  14456  cntzmhm  14830  gsumzaddlem  15219  dmdprdd  15253  dprdfeq0  15273  dprdres  15279  dprdss  15280  dprdz  15281  subgdmdprd  15285  dprd2dlem1  15292  dprd2da  15293  dmdprdsplit2lem  15296  lmhmlsp  15822  cnclsi  17017  cnprest2  17034  paste  17038  cmpfi  17151  conima  17167  1stcfb  17187  1stckgenlem  17264  kgencn3  17269  xkoco1cn  17367  xkoco2cn  17368  xkococnlem  17369  qtopval2  17403  basqtop  17418  imastopn  17427  kqopn  17441  kqcld  17442  hmeontr  17476  hmeores  17478  hmphdis  17503  cmphaushmeo  17507  qtopf1  17523  fbasrn  17595  uzfbas  17609  elfm  17658  elfm3  17661  imaelfm  17662  rnelfm  17664  tgpconcomp  17811  divstgpopn  17818  tsmsf1o  17843  qtopbaslem  18283  tgqioo  18322  cnheiborlem  18468  bndth  18472  fmcfil  18714  ovoliunlem1  18877  volsup  18929  uniioombllem4  18957  uniioombllem5  18958  opnmblALT  18974  volsup2  18976  mbfimaopnlem  19026  mbflimsup  19037  itg2gt0  19131  c1liplem1  19359  dvcnvrelem2  19381  mdegleb  19466  mdeglt  19467  mdegldg  19468  mdegxrcl  19469  mdegcl  19471  ig1peu  19573  efifo  19925  dvlog  20014  efopnlem2  20020  efopn  20021  subgornss  20989  ghsubgolem  21053  htthlem  21513  shsss  21908  imaelshi  22654  pjimai  22772  ballotlemsima  23090  ballotlemro  23097  coinfliprv  23698  erdsze2lem2  23750  eupares  23914  eupath2lem3  23918  nocvxminlem  24415  nocvxmin  24416  nobndlem1  24417  nobndlem2  24418  axcontlem10  24673  itg2addnclem2  25004  itg2gt0cn  25006  cmptdst  25671  limptlimpr2lem2  25678  supbrr  25739  tailf  26427  ismtyima  26630  ismtyres  26635  heibor1lem  26636  reheibor  26666  funsnfsup  26865  elrfirn  26873  isnacs2  26884  isnacs3  26888  fnwe2lem2  27251  lmhmfgima  27285  frlmsslsp  27351  lindff1  27393  lindfrn  27394  f1lindf  27395  lindfmm  27400  lsslindf  27403  f1omvdconj  27492  psgnunilem1  27519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-xp 4711  df-cnv 4713  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718
  Copyright terms: Public domain W3C validator