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

Theorem imaexg 6744
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 5199 . 2  |-  ( A
" B )  C_  ran  A
2 rnexg 6739 . 2  |-  ( A  e.  V  ->  ran  A  e.  _V )
3 ssexg 4571 . 2  |-  ( ( ( A " B
)  C_  ran  A  /\  ran  A  e.  _V )  ->  ( A " B
)  e.  _V )
41, 2, 3sylancr 667 1  |-  ( A  e.  V  ->  ( A " B )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   _Vcvv 3087    C_ wss 3442   ran crn 4855   "cima 4857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-xp 4860  df-cnv 4862  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867
This theorem is referenced by:  frxp  6917  ecexg  7375  pw2f1o  7683  fopwdom  7686  ssenen  7752  fiint  7854  fissuni  7885  fipreima  7886  marypha1lem  7953  infxpenlem  8443  ackbij2lem2  8668  enfin2i  8749  fin1a2lem7  8834  fpwwe  9070  canthwelem  9074  tskuni  9207  isacs4lem  16365  gsumvalx  16464  gicsubgen  16893  gsumzaddlem  17489  gsum2dlem1  17537  gsum2dlem2  17538  gsum2d  17539  isunit  17820  evpmss  19085  psgnevpmb  19086  ptbasfi  20527  xkococnlem  20605  qtopval  20641  hmphdis  20742  ustuqtop0  21186  ustuqtop4  21190  utopsnneiplem  21193  utopsnnei  21195  fmucnd  21238  neipcfilu  21242  metustel  21496  metustss  21497  metustfbas  21503  metuel2  21511  psmetutop  21513  restmetu  21516  nghmfval  21654  cnheiborlem  21878  itg2gt0  22595  fta1glem2  22992  fta1blem  22994  lgsqrlem4  24135  legval  24489  shsval  26800  nlfnval  27369  ffsrn  28157  gsummpt2co  28381  gsummpt2d  28382  locfinreflem  28506  qqhval  28617  esum2d  28753  mbfmcnt  28929  sitgaddlemb  29009  eulerpartgbij  29031  eulerpartlemgs2  29039  orvcval  29116  coinfliprv  29141  ballotlemrval  29176  ballotlem7  29194  msrval  29964  mthmval  30001  dfrdg2  30229  brapply  30490  dfrdg4  30503  tailval  30814  bj-clex  31307  isbasisrelowl  31495  relowlpssretop  31501  ptrest  31643  lkrval  32363  isnacs3  35261  pw2f1ocnv  35598  pw2f1o2val  35600  lmhmlnmsplit  35651  intima0  35878  elintima  35884  brtrclfv2  35958  frege98  36194  frege110  36206  frege133  36229  binomcxplemnotnn0  36342  sge0f1o  37758
  Copyright terms: Public domain W3C validator