Theorem imaexg 7914

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3464   ⊆ wss 3931  ran crn 5660   “ cima 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is referenced by:  imaex  7915  imaexd  7917  ecexg  8728  fopwdom  9099  gsumvalx  18659  gsum2dlem1  19956  gsum2dlem2  19957  gsum2d  19958  xkococnlem  23602  qtopval  23638  ustuqtop4  24188  utopsnnei  24193  fmucnd  24235  metustel  24494  metustss  24495  metustfbas  24501  metuel2  24509  psmetutop  24511  restmetu  24514  cnheiborlem  24909  itg2gt0  25718  shsval  31298  nlfnval  31867  fnpreimac  32654  ffsrn  32711  pwrssmgc  32985  gsummpt2co  33047  gsummpt2d  33048  qusima  33428  elrspunidl  33448  ply1degltdimlem  33667  algextdeglem8  33763  locfinreflem  33876  zarcmplem  33917  rhmpreimacnlem  33920  qqhval  34008  esum2d  34129  mbfmcnt  34305  sitgaddlemb  34385  eulerpartgbij  34409  eulerpartlemgs2  34417  orvcval  34495  coinfliprv  34520  ballotlemrval  34555  ballotlem7  34573  msrval  35565  mthmval  35602  dfrdg2  35818  tailval  36396  bj-clexab  36987  bj-imdirco  37213  isbasisrelowl  37381  relowlpssretop  37387  lkrval  39111  hashscontpow  42140  imacrhmcl  42512  isnacs3  42708  pw2f1ocnv  43036  pw2f1o2val  43038  lmhmlnmsplit  43086  frege98  43960  frege110  43972  frege133  43995  binomcxplemnotnn0  44355  tgqioo2  45556  smfco  46811  preimafvelsetpreimafv  47382  fundcmpsurinjlem2  47393