Theorem imaexg 7888

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3473   ⊆ wss 3944  ran crn 5670   “ cima 5672

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-xp 5675  df-cnv 5677  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682

This theorem is referenced by:  imaex  7889  ecexg  8690  fopwdom  9063  gsumvalx  18577  gsum2dlem1  19797  gsum2dlem2  19798  gsum2d  19799  xkococnlem  23092  qtopval  23128  ustuqtop4  23678  utopsnnei  23683  fmucnd  23726  metustel  23988  metustss  23989  metustfbas  23995  metuel2  24003  psmetutop  24005  restmetu  24008  cnheiborlem  24399  itg2gt0  25207  shsval  30428  nlfnval  30997  fnpreimac  31765  imaexd  31774  ffsrn  31825  pwrssmgc  32041  gsummpt2co  32071  gsummpt2d  32072  qusima  32376  elrspunidl  32397  ply1degltdimlem  32545  locfinreflem  32651  zarcmplem  32692  rhmpreimacnlem  32695  qqhval  32785  esum2d  32922  mbfmcnt  33098  sitgaddlemb  33178  eulerpartgbij  33202  eulerpartlemgs2  33210  orvcval  33287  coinfliprv  33312  ballotlemrval  33347  ballotlem7  33365  msrval  34360  mthmval  34397  dfrdg2  34597  tailval  35062  bj-clexab  35649  bj-imdirco  35875  isbasisrelowl  36043  relowlpssretop  36049  lkrval  37763  imacrhmcl  40893  isnacs3  41219  pw2f1ocnv  41547  pw2f1o2val  41549  lmhmlnmsplit  41600  frege98  42483  frege110  42495  frege133  42518  binomcxplemnotnn0  42886  imaexi  43691  tgqioo2  44033  sge0f1o  44871  smfco  45291  preimafvelsetpreimafv  45828  fundcmpsurinjlem2  45839  isomuspgrlem2a  46268