Theorem imaexg 7620

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 5940	. 2 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
2		rnexg 7614	. 2 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
3		ssexg 5227	. 2 ⊢ (((𝐴 “ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V) → (𝐴 “ 𝐵) ∈ V)
4	1, 2, 3	sylancr 589	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494   ⊆ wss 3936  ran crn 5556   “ cima 5558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568

This theorem is referenced by:  imaex  7621  ecexg  8293  fopwdom  8625  gsumvalx  17886  gsum2dlem1  19090  gsum2dlem2  19091  gsum2d  19092  xkococnlem  22267  qtopval  22303  ustuqtop4  22853  utopsnnei  22858  fmucnd  22901  metustel  23160  metustss  23161  metustfbas  23167  metuel2  23175  psmetutop  23177  restmetu  23180  cnheiborlem  23558  itg2gt0  24361  shsval  29089  nlfnval  29658  fnpreimac  30416  ffsrn  30465  gsummpt2co  30686  gsummpt2d  30687  locfinreflem  31104  qqhval  31215  esum2d  31352  mbfmcnt  31526  sitgaddlemb  31606  eulerpartgbij  31630  eulerpartlemgs2  31638  orvcval  31715  coinfliprv  31740  ballotlemrval  31775  ballotlem7  31793  msrval  32785  mthmval  32822  dfrdg2  33040  tailval  33721  bj-clex  34279  isbasisrelowl  34642  relowlpssretop  34648  lkrval  36239  isnacs3  39327  pw2f1ocnv  39654  pw2f1o2val  39656  lmhmlnmsplit  39707  frege98  40327  frege110  40339  frege133  40362  binomcxplemnotnn0  40708  imaexi  41506  tgqioo2  41843  sge0f1o  42684  smfco  43097  preimafvelsetpreimafv  43568  fundcmpsurinjlem2  43579  isomuspgrlem2a  44013