Theorem imaexg 7865

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 6038	. 2 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
2		rnexg 7854	. 2 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
3		ssexg 5270	. 2 ⊢ (((𝐴 “ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V) → (𝐴 “ 𝐵) ∈ V)
4	1, 2, 3	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  ran crn 5633   “ cima 5635

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 5243  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  imaex  7866  imaexd  7868  ecexg  8649  fopwdom  9025  gsumvalx  18613  gsum2dlem1  19911  gsum2dlem2  19912  gsum2d  19913  xkococnlem  23615  qtopval  23651  ustuqtop4  24200  utopsnnei  24205  fmucnd  24247  metustel  24506  metustss  24507  metustfbas  24513  metuel2  24521  psmetutop  24523  restmetu  24526  cnheiborlem  24921  itg2gt0  25729  shsval  31399  nlfnval  31968  fnpreimac  32759  ffsrn  32817  pwrssmgc  33092  gsummpt2co  33141  gsummpt2d  33142  qusima  33500  elrspunidl  33520  ply1degltdimlem  33799  algextdeglem8  33901  locfinreflem  34017  zarcmplem  34058  rhmpreimacnlem  34061  qqhval  34149  esum2d  34270  mbfmcnt  34445  sitgaddlemb  34525  eulerpartgbij  34549  eulerpartlemgs2  34557  orvcval  34635  coinfliprv  34660  ballotlemrval  34695  ballotlem7  34713  msrval  35751  mthmval  35788  dfrdg2  36006  tailval  36586  bj-clexab  37206  bj-imdirco  37439  isbasisrelowl  37607  relowlpssretop  37613  lkrval  39458  hashscontpow  42486  imacrhmcl  42878  isnacs3  43061  pw2f1ocnv  43388  pw2f1o2val  43390  lmhmlnmsplit  43438  frege98  44311  frege110  44323  frege133  44346  binomcxplemnotnn0  44706  tgqioo2  45901  smfco  47154  preimafvelsetpreimafv  47742  fundcmpsurinjlem2  47753