Theorem imaexg 7857

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	⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Proof of Theorem imaexg

Step	Hyp	Ref	Expression
1		imassrn 6030	. 2 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
2		rnexg 7846	. 2 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
3		ssexg 5260	. 2 ⊢ (((𝐴 “ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V) → (𝐴 “ 𝐵) ∈ V)
4	1, 2, 3	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  ran crn 5625   “ cima 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  imaex  7858  imaexd  7860  ecexg  8640  fopwdom  9016  gsumvalx  18635  gsum2dlem1  19936  gsum2dlem2  19937  gsum2d  19938  xkococnlem  23634  qtopval  23670  ustuqtop4  24219  utopsnnei  24224  fmucnd  24266  metustel  24525  metustss  24526  metustfbas  24532  metuel2  24540  psmetutop  24542  restmetu  24545  cnheiborlem  24931  itg2gt0  25737  shsval  31398  nlfnval  31967  fnpreimac  32758  ffsrn  32816  pwrssmgc  33075  gsummpt2co  33124  gsummpt2d  33125  qusima  33483  elrspunidl  33503  ply1degltdimlem  33782  algextdeglem8  33884  locfinreflem  34000  zarcmplem  34041  rhmpreimacnlem  34044  qqhval  34132  esum2d  34253  mbfmcnt  34428  sitgaddlemb  34508  eulerpartgbij  34532  eulerpartlemgs2  34540  orvcval  34618  coinfliprv  34643  ballotlemrval  34678  ballotlem7  34696  msrval  35736  mthmval  35773  dfrdg2  35991  tailval  36571  bj-clexab  37287  bj-imdirco  37520  isbasisrelowl  37688  relowlpssretop  37694  lkrval  39548  hashscontpow  42575  imacrhmcl  42973  isnacs3  43156  pw2f1ocnv  43483  pw2f1o2val  43485  lmhmlnmsplit  43533  frege98  44406  frege110  44418  frege133  44441  binomcxplemnotnn0  44801  tgqioo2  45995  smfco  47248  preimafvelsetpreimafv  47860  fundcmpsurinjlem2  47871