Theorem imaexg 7762

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3431   ⊆ wss 3888  ran crn 5592   “ cima 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5225  ax-nul 5232  ax-pr 5354  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5077  df-opab 5139  df-xp 5597  df-cnv 5599  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604

This theorem is referenced by:  imaex  7763  ecexg  8500  fopwdom  8865  gsumvalx  18358  gsum2dlem1  19569  gsum2dlem2  19570  gsum2d  19571  xkococnlem  22808  qtopval  22844  ustuqtop4  23394  utopsnnei  23399  fmucnd  23442  metustel  23704  metustss  23705  metustfbas  23711  metuel2  23719  psmetutop  23721  restmetu  23724  cnheiborlem  24115  itg2gt0  24923  shsval  29671  nlfnval  30240  fnpreimac  31005  ffsrn  31061  pwrssmgc  31275  gsummpt2co  31305  gsummpt2d  31306  qusima  31591  elrspunidl  31603  locfinreflem  31787  zarcmplem  31828  rhmpreimacnlem  31831  qqhval  31921  esum2d  32058  mbfmcnt  32232  sitgaddlemb  32312  eulerpartgbij  32336  eulerpartlemgs2  32344  orvcval  32421  coinfliprv  32446  ballotlemrval  32481  ballotlem7  32499  msrval  33497  mthmval  33534  dfrdg2  33768  tailval  34559  bj-clex  35151  bj-imdirco  35358  isbasisrelowl  35526  relowlpssretop  35532  lkrval  37099  isnacs3  40529  pw2f1ocnv  40856  pw2f1o2val  40858  lmhmlnmsplit  40909  frege98  41539  frege110  41551  frege133  41574  binomcxplemnotnn0  41944  imaexi  42731  tgqioo2  43055  sge0f1o  43890  smfco  44303  preimafvelsetpreimafv  44807  fundcmpsurinjlem2  44818  isomuspgrlem2a  45247