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

Theorem imaexg 4979
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 4978 . 2  |-  ( A
" B )  C_  ran  A
2 rnexg 4893 . 2  |-  ( A  e.  V  ->  ran  A  e.  _V )
3 ssexg 4100 . 2  |-  ( ( ( A " B
)  C_  ran  A  /\  ran  A  e.  _V )  ->  ( A " B
)  e.  _V )
41, 2, 3sylancr 647 1  |-  ( A  e.  V  ->  ( A " B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   _Vcvv 2740    C_ wss 3094   ran crn 4627   "cima 4629
This theorem is referenced by:  frxp  6124  ecexg  6597  pw2f1o  6900  fopwdom  6903  ssenen  6968  fiint  7066  fissuni  7093  fipreima  7094  marypha1lem  7119  cantnfdm  7298  cantnfcl  7301  cantnfval  7302  cantnflt2  7307  cantnff  7308  cantnflem1  7324  cnfcom2  7338  cnfcom3lem  7339  cnfcom3  7340  infxpenlem  7574  ackbij2lem2  7799  enfin2i  7880  fin1a2lem7  7965  fpwwe  8201  canthwelem  8205  tskuni  8338  isacs4lem  14198  gsumvalx  14378  gicsubgen  14669  gsumzaddlem  15130  gsum2d  15150  isunit  15366  ptbasfi  17203  xkococnlem  17280  qtopval  17313  hmphdis  17414  nghmfval  18158  cnheiborlem  18379  itg2gt0  19042  fta1glem2  19479  fta1blem  19481  lgsqrlem4  20510  shsval  21816  nlfnval  22386  ballotlemrval  23002  ballotlem7  23020  dfrdg2  23486  brapply  23817  dfrdg4  23828  intopcoaconb  24872  intopcoaconc  24873  prcnt  24883  nds  25482  tailval  25654  isnacs3  26117  pw2f1ocnv  26462  pw2f1o2val  26464  lmhmlnmsplit  26517  lkrval  28408
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-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152  ax-un 4449
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 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-xp 4640  df-cnv 4642  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647
  Copyright terms: Public domain W3C validator