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

Theorem imassrn 5024
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem imassrn
StepHypRef Expression
1 simpr 449 . . . 4  |-  ( ( x  e.  B  /\  <.
x ,  y >.  e.  A )  ->  <. x ,  y >.  e.  A
)
21eximi 1564 . . 3  |-  ( E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
)  ->  E. x <. x ,  y >.  e.  A )
32ss2abi 3246 . 2  |-  { y  |  E. x ( x  e.  B  /\  <.
x ,  y >.  e.  A ) }  C_  { y  |  E. x <. x ,  y >.  e.  A }
4 dfima3 5014 . 2  |-  ( A
" B )  =  { y  |  E. x ( x  e.  B  /\  <. x ,  y >.  e.  A
) }
5 dfrn3 4868 . 2  |-  ran  A  =  { y  |  E. x <. x ,  y
>.  e.  A }
63, 4, 53sstr4i 3218 1  |-  ( A
" B )  C_  ran  A
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1529    e. wcel 1685   {cab 2270    C_ wss 3153   <.cop 3644   ran crn 4689   "cima 4691
This theorem is referenced by:  imaexg  5025  0ima  5030  cnvimass  5032  fimacnv  5618  isofrlem  5798  isofr2  5802  f1oweALT  5812  f1opw2  6032  frxp  6186  smores2  6366  ecss  6696  f1imaen2g  6917  domunsncan  6957  fopwdom  6965  sbthlem2  6967  sbthlem3  6968  sbthlem5  6970  sbthlem6  6971  ssenen  7030  ssfi  7078  fiint  7128  f1opwfi  7154  fissuni  7155  fipreima  7156  marypha1lem  7181  unxpwdom2  7297  tz9.12lem1  7454  acndom2  7676  dfac12lem2  7765  isf34lem5  7999  isf34lem7  8000  isf34lem6  8001  enfin1ai  8005  hsmexlem4  8050  hsmexlem5  8051  fpwwe2lem6  8252  fpwwe2lem9  8255  tskuni  8400  limsupgle  11945  limsupval2  11948  limsupgre  11949  isercolllem2  12133  isercoll  12135  unbenlem  12949  imasless  13436  isacs1i  13553  isacs4lem  14265  mhmima  14434  cntzmhm  14808  gsumzaddlem  15197  dmdprdd  15231  dprdfeq0  15251  dprdres  15257  dprdss  15258  dprdz  15259  subgdmdprd  15263  dprd2dlem1  15270  dprd2da  15271  dmdprdsplit2lem  15274  lmhmlsp  15800  cnclsi  16995  cnprest2  17012  paste  17016  cmpfi  17129  conima  17145  1stcfb  17165  1stckgenlem  17242  kgencn3  17247  xkoco1cn  17345  xkoco2cn  17346  xkococnlem  17347  qtopval2  17381  basqtop  17396  imastopn  17405  kqopn  17419  kqcld  17420  hmeontr  17454  hmeores  17456  hmphdis  17481  cmphaushmeo  17485  qtopf1  17501  fbasrn  17573  uzfbas  17587  elfm  17636  elfm3  17639  imaelfm  17640  rnelfm  17642  tgpconcomp  17789  divstgpopn  17796  tsmsf1o  17821  qtopbaslem  18261  tgqioo  18300  cnheiborlem  18446  bndth  18450  fmcfil  18692  ovoliunlem1  18855  volsup  18907  uniioombllem4  18935  uniioombllem5  18936  opnmblALT  18952  volsup2  18954  mbfimaopnlem  19004  mbflimsup  19015  itg2gt0  19109  c1liplem1  19337  dvcnvrelem2  19359  mdegleb  19444  mdeglt  19445  mdegldg  19446  mdegxrcl  19447  mdegcl  19449  ig1peu  19551  efifo  19903  dvlog  19992  efopnlem2  19998  efopn  19999  subgornss  20965  ghsubgolem  21029  htthlem  21489  shsss  21884  imaelshi  22630  pjimai  22748  ballotlemsima  23067  ballotlemro  23074  erdsze2lem2  23139  eupares  23303  eupath2lem3  23307  nocvxminlem  23745  nocvxmin  23746  axfelem1  23747  axfelem2  23748  axcontlem10  24008  cmptdst  24967  limptlimpr2lem2  24974  supbrr  25035  tailf  25723  ismtyima  25926  ismtyres  25931  heibor1lem  25932  reheibor  25962  funsnfsup  26161  elrfirn  26169  isnacs2  26180  isnacs3  26184  fnwe2lem2  26547  lmhmfgima  26581  frlmsslsp  26647  lindff1  26689  lindfrn  26690  f1lindf  26691  lindfmm  26696  lsslindf  26699  f1omvdconj  26788  psgnunilem1  26815
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-xp 4694  df-cnv 4696  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701
  Copyright terms: Public domain W3C validator