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

Theorem imaexg 5159
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 5158 . 2  |-  ( A
" B )  C_  ran  A
2 rnexg 5073 . 2  |-  ( A  e.  V  ->  ran  A  e.  _V )
3 ssexg 4292 . 2  |-  ( ( ( A " B
)  C_  ran  A  /\  ran  A  e.  _V )  ->  ( A " B
)  e.  _V )
41, 2, 3sylancr 645 1  |-  ( A  e.  V  ->  ( A " B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   _Vcvv 2901    C_ wss 3265   ran crn 4821   "cima 4823
This theorem is referenced by:  frxp  6394  ecexg  6847  pw2f1o  7151  fopwdom  7154  ssenen  7219  fiint  7321  fissuni  7348  fipreima  7349  marypha1lem  7375  cantnfdm  7554  cantnfcl  7557  cantnfval  7558  cantnff  7564  cantnflem1  7580  cnfcom2  7594  cnfcom3lem  7595  cnfcom3  7596  infxpenlem  7830  ackbij2lem2  8055  enfin2i  8136  fin1a2lem7  8221  fpwwe  8456  canthwelem  8460  tskuni  8593  isacs4lem  14523  gsumvalx  14703  gicsubgen  14994  gsumzaddlem  15455  gsum2d  15475  isunit  15691  ptbasfi  17536  xkococnlem  17614  qtopval  17650  hmphdis  17751  ustuqtop0  18193  ustuqtop4  18197  utopsnneiplem  18200  utopsnnei  18202  fmucnd  18245  neipcfilu  18249  metustel  18472  metustss  18473  metustfbas  18479  metuel2  18487  metutop  18489  restmetu  18491  nghmfval  18629  cnheiborlem  18852  itg2gt0  19521  fta1glem2  19958  fta1blem  19960  lgsqrlem4  20997  shsval  22664  nlfnval  23234  qqhval  24159  mbfmcnt  24414  orvcval  24496  coinfliprv  24521  ballotlemrval  24556  ballotlem7  24574  dfrdg2  25178  brapply  25503  dfrdg4  25515  tailval  26095  isnacs3  26457  pw2f1ocnv  26801  pw2f1o2val  26803  lmhmlnmsplit  26856  lkrval  29205
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346  ax-un 4643
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-xp 4826  df-cnv 4828  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833
  Copyright terms: Public domain W3C validator