Theorem imaexg 7936

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3479   ⊆ wss 3950  ran crn 5685   “ cima 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-xp 5690  df-cnv 5692  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697

This theorem is referenced by:  imaex  7937  imaexd  7939  ecexg  8750  fopwdom  9121  gsumvalx  18690  gsum2dlem1  19989  gsum2dlem2  19990  gsum2d  19991  xkococnlem  23668  qtopval  23704  ustuqtop4  24254  utopsnnei  24259  fmucnd  24302  metustel  24564  metustss  24565  metustfbas  24571  metuel2  24579  psmetutop  24581  restmetu  24584  cnheiborlem  24987  itg2gt0  25796  shsval  31332  nlfnval  31901  fnpreimac  32682  ffsrn  32741  pwrssmgc  32991  gsummpt2co  33052  gsummpt2d  33053  qusima  33437  elrspunidl  33457  ply1degltdimlem  33674  algextdeglem8  33766  locfinreflem  33840  zarcmplem  33881  rhmpreimacnlem  33884  qqhval  33974  esum2d  34095  mbfmcnt  34271  sitgaddlemb  34351  eulerpartgbij  34375  eulerpartlemgs2  34383  orvcval  34461  coinfliprv  34486  ballotlemrval  34521  ballotlem7  34539  msrval  35544  mthmval  35581  dfrdg2  35797  tailval  36375  bj-clexab  36966  bj-imdirco  37192  isbasisrelowl  37360  relowlpssretop  37366  lkrval  39090  hashscontpow  42124  imacrhmcl  42529  isnacs3  42726  pw2f1ocnv  43054  pw2f1o2val  43056  lmhmlnmsplit  43104  frege98  43979  frege110  43991  frege133  44014  binomcxplemnotnn0  44380  tgqioo2  45565  smfco  46822  preimafvelsetpreimafv  47380  fundcmpsurinjlem2  47391