Theorem imaexg 7849

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3437   ⊆ wss 3898  ran crn 5620   “ cima 5622

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 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  imaex  7850  imaexd  7852  ecexg  8632  fopwdom  9005  gsumvalx  18586  gsum2dlem1  19884  gsum2dlem2  19885  gsum2d  19886  xkococnlem  23575  qtopval  23611  ustuqtop4  24160  utopsnnei  24165  fmucnd  24207  metustel  24466  metustss  24467  metustfbas  24473  metuel2  24481  psmetutop  24483  restmetu  24486  cnheiborlem  24881  itg2gt0  25689  shsval  31294  nlfnval  31863  fnpreimac  32655  ffsrn  32715  pwrssmgc  32988  gsummpt2co  33035  gsummpt2d  33036  qusima  33380  elrspunidl  33400  ply1degltdimlem  33656  algextdeglem8  33758  locfinreflem  33874  zarcmplem  33915  rhmpreimacnlem  33918  qqhval  34006  esum2d  34127  mbfmcnt  34302  sitgaddlemb  34382  eulerpartgbij  34406  eulerpartlemgs2  34414  orvcval  34492  coinfliprv  34517  ballotlemrval  34552  ballotlem7  34570  msrval  35603  mthmval  35640  dfrdg2  35858  tailval  36438  bj-clexab  37029  bj-imdirco  37255  isbasisrelowl  37423  relowlpssretop  37429  lkrval  39208  hashscontpow  42236  imacrhmcl  42633  isnacs3  42828  pw2f1ocnv  43155  pw2f1o2val  43157  lmhmlnmsplit  43205  frege98  44079  frege110  44091  frege133  44114  binomcxplemnotnn0  44474  tgqioo2  45672  smfco  46925  preimafvelsetpreimafv  47513  fundcmpsurinjlem2  47524