Theorem imaexg 7855

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901  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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  imaex  7856  imaexd  7858  ecexg  8639  fopwdom  9013  gsumvalx  18601  gsum2dlem1  19899  gsum2dlem2  19900  gsum2d  19901  xkococnlem  23603  qtopval  23639  ustuqtop4  24188  utopsnnei  24193  fmucnd  24235  metustel  24494  metustss  24495  metustfbas  24501  metuel2  24509  psmetutop  24511  restmetu  24514  cnheiborlem  24909  itg2gt0  25717  shsval  31387  nlfnval  31956  fnpreimac  32749  ffsrn  32807  pwrssmgc  33082  gsummpt2co  33131  gsummpt2d  33132  qusima  33489  elrspunidl  33509  ply1degltdimlem  33779  algextdeglem8  33881  locfinreflem  33997  zarcmplem  34038  rhmpreimacnlem  34041  qqhval  34129  esum2d  34250  mbfmcnt  34425  sitgaddlemb  34505  eulerpartgbij  34529  eulerpartlemgs2  34537  orvcval  34615  coinfliprv  34640  ballotlemrval  34675  ballotlem7  34693  msrval  35732  mthmval  35769  dfrdg2  35987  tailval  36567  bj-clexab  37165  bj-imdirco  37391  isbasisrelowl  37559  relowlpssretop  37565  lkrval  39344  hashscontpow  42372  imacrhmcl  42765  isnacs3  42948  pw2f1ocnv  43275  pw2f1o2val  43277  lmhmlnmsplit  43325  frege98  44198  frege110  44210  frege133  44233  binomcxplemnotnn0  44593  tgqioo2  45789  smfco  47042  preimafvelsetpreimafv  47630  fundcmpsurinjlem2  47641