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

Theorem imaexg 4933
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 4932 . 2  |-  ( A
" B )  C_  ran  A
2 rnexg 4847 . 2  |-  ( A  e.  V  ->  ran  A  e.  _V )
3 ssexg 4057 . 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 2727    C_ wss 3078   ran crn 4581   "cima 4583
This theorem is referenced by:  frxp  6077  ecexg  6550  pw2f1o  6852  fopwdom  6855  ssenen  6920  fiint  7018  fissuni  7044  fipreima  7045  marypha1lem  7070  cantnfdm  7249  cantnfcl  7252  cantnfval  7253  cantnflt2  7258  cantnff  7259  cantnflem1  7275  cnfcom2  7289  cnfcom3lem  7290  cnfcom3  7291  infxpenlem  7525  ackbij2lem2  7750  enfin2i  7831  fin1a2lem7  7916  fpwwe  8148  canthwelem  8152  tskuni  8285  isacs4lem  14115  gsumvalx  14286  gicsubgen  14577  gsumzaddlem  15038  gsum2d  15058  isunit  15274  ptbasfi  17108  xkococnlem  17185  qtopval  17218  hmphdis  17319  nghmfval  18063  cnheiborlem  18284  itg2gt0  18947  fta1glem2  19384  fta1blem  19386  lgsqrlem4  20415  shsval  21721  nlfnval  22291  dfrdg2  23320  brapply  23651  dfrdg4  23662  intopcoaconb  24706  intopcoaconc  24707  prcnt  24717  nds  25316  tailval  25488  isnacs3  25951  pw2f1ocnv  26296  pw2f1o2val  26298  lmhmlnmsplit  26351  lkrval  27967
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601
  Copyright terms: Public domain W3C validator