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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  ran crn 5623   “ cima 5625

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 2709  ax-sep 5231  ax-pr 5368  ax-un 7680

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5628  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635

This theorem is referenced by:  imaex  7856  imaexd  7858  ecexg  8638  fopwdom  9014  gsumvalx  18602  gsum2dlem1  19903  gsum2dlem2  19904  gsum2d  19905  xkococnlem  23602  qtopval  23638  ustuqtop4  24187  utopsnnei  24192  fmucnd  24234  metustel  24493  metustss  24494  metustfbas  24500  metuel2  24508  psmetutop  24510  restmetu  24513  cnheiborlem  24899  itg2gt0  25705  shsval  31372  nlfnval  31941  fnpreimac  32732  ffsrn  32790  pwrssmgc  33065  gsummpt2co  33114  gsummpt2d  33115  qusima  33473  elrspunidl  33493  ply1degltdimlem  33772  algextdeglem8  33874  locfinreflem  33990  zarcmplem  34031  rhmpreimacnlem  34034  qqhval  34122  esum2d  34243  mbfmcnt  34418  sitgaddlemb  34498  eulerpartgbij  34522  eulerpartlemgs2  34530  orvcval  34608  coinfliprv  34633  ballotlemrval  34668  ballotlem7  34686  msrval  35726  mthmval  35763  dfrdg2  35981  tailval  36561  bj-clexab  37269  bj-imdirco  37502  isbasisrelowl  37670  relowlpssretop  37676  lkrval  39525  hashscontpow  42553  imacrhmcl  42958  isnacs3  43141  pw2f1ocnv  43468  pw2f1o2val  43470  lmhmlnmsplit  43518  frege98  44391  frege110  44403  frege133  44426  binomcxplemnotnn0  44786  tgqioo2  45981  smfco  47234  preimafvelsetpreimafv  47822  fundcmpsurinjlem2  47833