Theorem imaexg 7860

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 7849	. 2 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
3		ssexg 5258	. 2 ⊢ (((𝐴 “ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V) → (𝐴 “ 𝐵) ∈ V)
4	1, 2, 3	sylancr 593	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432   ⊆ wss 3890  ran crn 5626   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  imaex  7861  imaexd  7863  ecexg  8644  fopwdom  9020  gsumvalx  18642  gsum2dlem1  19943  gsum2dlem2  19944  gsum2d  19945  xkococnlem  23649  qtopval  23685  ustuqtop4  24234  utopsnnei  24239  fmucnd  24281  metustel  24540  metustss  24541  metustfbas  24547  metuel2  24555  psmetutop  24557  restmetu  24560  cnheiborlem  24946  itg2gt0  25752  shsval  31408  nlfnval  31977  fnpreimac  32769  ffsrn  32827  pwrssmgc  33086  gsummpt2co  33136  gsummpt2d  33137  qusima  33498  elrspunidl  33518  ply1degltdimlem  33813  algextdeglem8  33915  locfinreflem  34031  zarcmplem  34072  rhmpreimacnlem  34075  qqhval  34163  esum2d  34284  mbfmcnt  34459  sitgaddlemb  34539  eulerpartgbij  34563  eulerpartlemgs2  34571  orvcval  34649  coinfliprv  34674  ballotlemrval  34709  ballotlem7  34727  msrval  35773  mthmval  35810  dfrdg2  36028  tailval  36608  bj-clexab  37324  bj-imdirco  37557  isbasisrelowl  37727  relowlpssretop  37733  lkrval  39587  hashscontpow  42614  imacrhmcl  43011  isnacs3  43166  pw2f1ocnv  43489  pw2f1o2val  43491  lmhmlnmsplit  43539  frege98  44412  frege110  44424  frege133  44447  binomcxplemnotnn0  44807  tgqioo2  45999  smfco  47252  preimafvelsetpreimafv  47870  fundcmpsurinjlem2  47881