Theorem imaexg 7864

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 6036	. 2 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
2		rnexg 7853	. 2 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
3		ssexg 5264	. 2 ⊢ (((𝐴 “ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V) → (𝐴 “ 𝐵) ∈ V)
4	1, 2, 3	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889  ran crn 5632   “ cima 5634

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  imaex  7865  imaexd  7867  ecexg  8647  fopwdom  9023  gsumvalx  18644  gsum2dlem1  19945  gsum2dlem2  19946  gsum2d  19947  xkococnlem  23624  qtopval  23660  ustuqtop4  24209  utopsnnei  24214  fmucnd  24256  metustel  24515  metustss  24516  metustfbas  24522  metuel2  24530  psmetutop  24532  restmetu  24535  cnheiborlem  24921  itg2gt0  25727  shsval  31383  nlfnval  31952  fnpreimac  32743  ffsrn  32801  pwrssmgc  33060  gsummpt2co  33109  gsummpt2d  33110  qusima  33468  elrspunidl  33488  ply1degltdimlem  33766  algextdeglem8  33868  locfinreflem  33984  zarcmplem  34025  rhmpreimacnlem  34028  qqhval  34116  esum2d  34237  mbfmcnt  34412  sitgaddlemb  34492  eulerpartgbij  34516  eulerpartlemgs2  34524  orvcval  34602  coinfliprv  34627  ballotlemrval  34662  ballotlem7  34680  msrval  35720  mthmval  35757  dfrdg2  35975  tailval  36555  bj-clexab  37271  bj-imdirco  37504  isbasisrelowl  37674  relowlpssretop  37680  lkrval  39534  hashscontpow  42561  imacrhmcl  42959  isnacs3  43142  pw2f1ocnv  43465  pw2f1o2val  43467  lmhmlnmsplit  43515  frege98  44388  frege110  44400  frege133  44423  binomcxplemnotnn0  44783  tgqioo2  45977  smfco  47230  preimafvelsetpreimafv  47848  fundcmpsurinjlem2  47859