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

Theorem imaexg 5042
Description: The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by NM, 24-Jul-1995.)
Assertion
Ref Expression
imaexg  |-  ( A  e.  V  ->  ( A " B )  e. 
_V )

Proof of Theorem imaexg
StepHypRef Expression
1 imassrn 5041 . 2  |-  ( A
" B )  C_  ran  A
2 rnexg 4956 . 2  |-  ( A  e.  V  ->  ran  A  e.  _V )
3 ssexg 4176 . 2  |-  ( ( ( A " B
)  C_  ran  A  /\  ran  A  e.  _V )  ->  ( A " B
)  e.  _V )
41, 2, 3sylancr 644 1  |-  ( A  e.  V  ->  ( A " B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   _Vcvv 2801    C_ wss 3165   ran crn 4706   "cima 4708
This theorem is referenced by:  frxp  6241  ecexg  6680  pw2f1o  6983  fopwdom  6986  ssenen  7051  fiint  7149  fissuni  7176  fipreima  7177  marypha1lem  7202  cantnfdm  7381  cantnfcl  7384  cantnfval  7385  cantnflt2  7390  cantnff  7391  cantnflem1  7407  cnfcom2  7421  cnfcom3lem  7422  cnfcom3  7423  infxpenlem  7657  ackbij2lem2  7882  enfin2i  7963  fin1a2lem7  8048  fpwwe  8284  canthwelem  8288  tskuni  8421  isacs4lem  14287  gsumvalx  14467  gicsubgen  14758  gsumzaddlem  15219  gsum2d  15239  isunit  15455  ptbasfi  17292  xkococnlem  17369  qtopval  17402  hmphdis  17503  nghmfval  18247  cnheiborlem  18468  itg2gt0  19131  fta1glem2  19568  fta1blem  19570  lgsqrlem4  20599  shsval  21907  nlfnval  22477  ballotlemrval  23092  ballotlem7  23110  mbfmcnt  23588  orvcval  23673  coinfliprv  23698  dfrdg2  24223  brapply  24548  dfrdg4  24560  intopcoaconb  25643  intopcoaconc  25644  prcnt  25654  nds  26253  tailval  26425  isnacs3  26888  pw2f1ocnv  27233  pw2f1o2val  27235  lmhmlnmsplit  27288  lkrval  29900
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-13 1698  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  ax-un 4528
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-uni 3844  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