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

Theorem imassrn 5013
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
StepHypRef Expression
1 simpr 449 . . . 4  |-  ( ( x  e.  B  /\  <.
x ,  y >.  e.  A )  ->  <. x ,  y >.  e.  A
)
21eximi 1574 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
32ss2abi 3220 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
4 dfima3 5003 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
5 dfrn3 4857 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
63, 4, 53sstr4i 3192 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1537    e. wcel 1621   {cab 2244    C_ wss 3127   <.cop 3617   ran crn 4662   "cima 4664
This theorem is referenced by:  imaexg  5014  0ima  5019  cnvimass  5021  fimacnv  5591  isofrlem  5771  isofr2  5775  f1oweALT  5785  f1opw2  6005  frxp  6159  smores2  6339  ecss  6669  f1imaen2g  6890  domunsncan  6930  fopwdom  6938  sbthlem2  6940  sbthlem3  6941  sbthlem5  6943  sbthlem6  6944  ssenen  7003  ssfi  7051  fiint  7101  f1opwfi  7127  fissuni  7128  fipreima  7129  marypha1lem  7154  unxpwdom2  7270  tz9.12lem1  7427  acndom2  7649  dfac12lem2  7738  isf34lem5  7972  isf34lem7  7973  isf34lem6  7974  enfin1ai  7978  hsmexlem4  8023  hsmexlem5  8024  fpwwe2lem6  8225  fpwwe2lem9  8228  tskuni  8373  limsupgle  11916  limsupval2  11919  limsupgre  11920  isercolllem2  12104  isercoll  12106  unbenlem  12917  imasless  13404  isacs1i  13521  isacs4lem  14233  mhmima  14402  cntzmhm  14776  gsumzaddlem  15165  dmdprdd  15199  dprdfeq0  15219  dprdres  15225  dprdss  15226  dprdz  15227  subgdmdprd  15231  dprd2dlem1  15238  dprd2da  15239  dmdprdsplit2lem  15242  lmhmlsp  15768  cnclsi  16963  cnprest2  16980  paste  16984  cmpfi  17097  conima  17113  1stcfb  17133  1stckgenlem  17210  kgencn3  17215  xkoco1cn  17313  xkoco2cn  17314  xkococnlem  17315  qtopval2  17349  basqtop  17364  imastopn  17373  kqopn  17387  kqcld  17388  hmeontr  17422  hmeores  17424  hmphdis  17449  cmphaushmeo  17453  qtopf1  17469  fbasrn  17541  uzfbas  17555  elfm  17604  elfm3  17607  imaelfm  17608  rnelfm  17610  tgpconcomp  17757  divstgpopn  17764  tsmsf1o  17789  qtopbaslem  18229  tgqioo  18268  cnheiborlem  18414  bndth  18418  fmcfil  18660  ovoliunlem1  18823  volsup  18875  uniioombllem4  18903  uniioombllem5  18904  opnmblALT  18920  volsup2  18922  mbfimaopnlem  18972  mbflimsup  18983  itg2gt0  19077  c1liplem1  19305  dvcnvrelem2  19327  mdegleb  19412  mdeglt  19413  mdegldg  19414  mdegxrcl  19415  mdegcl  19417  ig1peu  19519  efifo  19871  dvlog  19960  efopnlem2  19966  efopn  19967  subgornss  20933  ghsubgolem  20997  htthlem  21457  shsss  21852  imaelshi  22598  pjimai  22716  ballotlemsima  23035  ballotlemro  23042  erdsze2lem2  23107  eupares  23271  eupath2lem3  23275  nocvxminlem  23713  nocvxmin  23714  axfelem1  23715  axfelem2  23716  axcontlem10  23976  cmptdst  24935  limptlimpr2lem2  24942  supbrr  25003  tailf  25691  ismtyima  25894  ismtyres  25899  heibor1lem  25900  reheibor  25930  funsnfsup  26129  elrfirn  26137  isnacs2  26148  isnacs3  26152  fnwe2lem2  26515  lmhmfgima  26549  frlmsslsp  26615  lindff1  26657  lindfrn  26658  f1lindf  26659  lindfmm  26664  lsslindf  26667  f1omvdconj  26756  psgnunilem1  26783
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-br 3998  df-opab 4052  df-xp 4675  df-cnv 4677  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682
  Copyright terms: Public domain W3C validator