Theorem imaexg 7910

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 6070	. 2 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
2		rnexg 7899	. 2 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
3		ssexg 5323	. 2 ⊢ (((𝐴 “ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V) → (𝐴 “ 𝐵) ∈ V)
4	1, 2, 3	sylancr 586	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3473   ⊆ wss 3948  ran crn 5677   “ cima 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689

This theorem is referenced by:  imaex  7911  ecexg  8713  fopwdom  9086  gsumvalx  18607  gsum2dlem1  19886  gsum2dlem2  19887  gsum2d  19888  xkococnlem  23483  qtopval  23519  ustuqtop4  24069  utopsnnei  24074  fmucnd  24117  metustel  24379  metustss  24380  metustfbas  24386  metuel2  24394  psmetutop  24396  restmetu  24399  cnheiborlem  24800  itg2gt0  25610  shsval  30998  nlfnval  31567  fnpreimac  32329  imaexd  32337  ffsrn  32387  pwrssmgc  32603  gsummpt2co  32636  gsummpt2d  32637  qusima  32959  elrspunidl  32986  ply1degltdimlem  33161  algextdeglem8  33235  locfinreflem  33284  zarcmplem  33325  rhmpreimacnlem  33328  qqhval  33418  esum2d  33555  mbfmcnt  33731  sitgaddlemb  33811  eulerpartgbij  33835  eulerpartlemgs2  33843  orvcval  33920  coinfliprv  33945  ballotlemrval  33980  ballotlem7  33998  msrval  34993  mthmval  35030  dfrdg2  35237  tailval  35722  bj-clexab  36309  bj-imdirco  36535  isbasisrelowl  36703  relowlpssretop  36709  lkrval  38422  imacrhmcl  41554  isnacs3  41911  pw2f1ocnv  42239  pw2f1o2val  42241  lmhmlnmsplit  42292  frege98  43175  frege110  43187  frege133  43210  binomcxplemnotnn0  43578  imaexi  44379  tgqioo2  44719  sge0f1o  45557  smfco  45977  preimafvelsetpreimafv  46515  fundcmpsurinjlem2  46526  isomuspgrlem2a  46955