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

Theorem imassrn 5195
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 1723 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
21ss2abi 3533 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
3 dfima3 5187 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
4 dfrn3 5040 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
52, 3, 43sstr4i 3503 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370   E.wex 1659    e. wcel 1868   {cab 2407    C_ wss 3436   <.cop 4002   ran crn 4851   "cima 4853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-xp 4856  df-cnv 4858  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863
This theorem is referenced by:  0ima  5200  cnvimass  5204  fimacnv  6024  isofrlem  6243  isofr2  6247  f1opw2  6533  imaexg  6741  f1oweALT  6788  frxp  6914  smores2  7078  ecss  7410  f1imaen2g  7634  domunsncan  7675  fopwdom  7683  sbthlem2  7686  sbthlem3  7687  sbthlem5  7689  sbthlem6  7690  ssenen  7749  ssfi  7795  fiint  7851  f1opwfi  7881  fissuni  7882  fipreima  7883  marypha1lem  7950  unxpwdom2  8106  tz9.12lem1  8260  acndom2  8486  dfac12lem2  8575  isf34lem5  8809  isf34lem7  8810  isf34lem6  8811  enfin1ai  8815  hsmexlem4  8860  hsmexlem5  8861  fpwwe2lem6  9061  fpwwe2lem9  9064  tskuni  9209  limsupgle  13523  limsupval2  13528  limsupval2OLD  13529  limsupgre  13530  limsupgreOLD  13531  isercolllem2  13717  isercoll  13719  unbenlem  14840  imasless  15434  isacs1i  15551  isacs4lem  16402  mhmima  16598  cntzmhm  16980  f1omvdconj  17075  psgnunilem1  17122  gsumzaddlem  17542  dmdprdd  17619  dprdfeq0  17643  dprdres  17649  dprdss  17650  dprdz  17651  subgdmdprd  17655  dprd2dlem1  17662  dprd2da  17663  dmdprdsplit2lem  17666  lmhmlsp  18260  frlmsslsp  19341  lindff1  19365  lindfrn  19366  f1lindf  19367  lindfmm  19372  lsslindf  19375  cnclsi  20275  cnprest2  20293  paste  20297  cmpfi  20410  conima  20427  1stcfb  20447  1stckgenlem  20555  kgencn3  20560  xkoco1cn  20659  xkoco2cn  20660  xkococnlem  20661  qtopval2  20698  basqtop  20713  imastopn  20722  kqopn  20736  kqcld  20737  hmeontr  20771  hmeores  20773  hmphdis  20798  cmphaushmeo  20802  qtopf1  20818  fbasrn  20886  uzfbas  20900  elfm  20949  elfm3  20952  imaelfm  20953  rnelfm  20955  cnextcn  21069  tgpconcomp  21114  qustgpopn  21121  tsmsf1o  21146  ustimasn  21230  utopbas  21237  restutop  21239  qtopbaslem  21766  tgqioo  21805  cnheiborlem  21969  bndth  21973  fmcfil  22229  ovoliunlem1  22442  volsup  22496  uniioombllem4  22531  uniioombllem5  22532  opnmblALT  22548  volsup2  22550  mbfimaopnlem  22598  mbflimsup  22610  mbflimsupOLD  22611  itg2gt0  22705  c1liplem1  22935  dvcnvrelem2  22957  mdegleb  23000  mdeglt  23001  mdegldg  23002  mdegxrcl  23003  mdegcl  23005  ig1peu  23109  ig1peuOLD  23110  efifo  23483  dvlog  23583  efopnlem2  23589  efopn  23590  f1otrg  24888  axcontlem10  24990  eupares  25689  eupath2lem3  25693  subgornss  26020  ghsubgolemOLD  26084  htthlem  26556  shsss  26952  imaelshi  27697  pjimai  27815  fimarab  28234  gsummpt2co  28538  sitgclbn  29172  sitgaddlemb  29177  eulerpartlemgvv  29205  eulerpartlemgf  29208  coinfliprv  29311  ballotlemsima  29344  ballotlemro  29351  ballotlemsimaOLD  29382  ballotlemroOLD  29389  erdsze2lem2  29923  mrsubrn  30147  msubrn  30163  nocvxminlem  30572  nocvxmin  30573  nobndlem1  30574  nobndlem2  30575  tailf  31024  dissneqlem  31683  poimirlem1  31855  poimirlem2  31856  poimirlem3  31857  poimirlem11  31865  poimirlem12  31866  poimirlem15  31869  poimirlem16  31870  poimirlem19  31873  poimirlem30  31884  itg2addnclem2  31908  itg2gt0cn  31911  ftc1anclem7  31937  ftc1anc  31939  ismtyima  32049  ismtyres  32054  heibor1lem  32055  reheibor  32085  elrfirn  35456  isnacs2  35467  isnacs3  35471  fnwe2lem2  35829  lmhmfgima  35862  brtrclfv2  36179  xphe  36234  imo72b2lem0  36466  imo72b2lem2  36468  imo72b2lem1  36472  imo72b2  36477  fimass  37292  limccog  37520  mgmhmima  39074
  Copyright terms: Public domain W3C validator