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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902  ran crn 5660   “ cima 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is used by:  imaex  7915  imaexd  7917  ecexg  8704  fopwdom  9087  gsumvalx  18784  gsum2dlem1  20103  gsum2dlem2  20104  gsum2d  20105  xkococnlem  23891  qtopval  23927  ustuqtop4  24476  utopsnnei  24481  fmucnd  24523  metustel  24782  metustss  24783  metustfbas  24789  metuel2  24797  psmetutop  24799  restmetu  24802  cnheiborlem  25188  itg2gt0  25994  shsval  31801  nlfnval  32370  fnpreimac  33151  pwrssmgc  33448  gsummpt2co  33496  gsummpt2d  33497  qusima  33845  elrspunidl  33864  ply1degltdimlem  34140  algextdeglem8  34242  locfinreflem  34358  zarcmplem  34399  rhmpreimacnlem  34402  qqhval  34490  esum2d  34611  mbfmcnt  34787  sitgaddlemb  34867  eulerpartgbij  34891  eulerpartlemgs2  34899  orvcval  34977  coinfliprv  35002  ballotlemrval  35037  ballotlem7  35055  msrval  36125  mthmval  36162  dfrdg2  36380  tailval  37000  bj-clexab  37716  bj-imdirco  37950  isbasisrelowl  38120  relowlpssretop  38126  lkrval  39969  hashscontpow  42996  imacrhmcl  43410  isnacs3  43563  pw2f1ocnv  43886  pw2f1o2val  43888  lmhmlnmsplit  43936  frege98  44809  frege110  44821  frege133  44844  binomcxplemnotnn0  45188  tgqioo2  46385  smfco  47638  preimafvelsetpreimafv  48296  fundcmpsurinjlem2  48307