Theorem imaexg 7926

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  ran crn 5651   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  imaex  7927  imaexd  7929  ecexg  8725  fopwdom  9108  gsumvalx  18871  gsum2dlem1  20190  gsum2dlem2  20191  gsum2d  20192  xkococnlem  23984  qtopval  24020  ustuqtop4  24569  utopsnnei  24574  fmucnd  24616  metustel  24875  metustss  24876  metustfbas  24882  metuel2  24890  psmetutop  24892  restmetu  24895  cnheiborlem  25281  itg2gt0  26087  shsval  31920  nlfnval  32489  fnpreimac  33312  pwrssmgc  33608  gsummpt2co  33656  gsummpt2d  33657  qusima  34006  ply1degltdimlem  34301  algextdeglem8  34403  locfinreflem  34519  zarcmplem  34560  rhmpreimacnlem  34563  qqhval  34651  esum2d  34772  mbfmcnt  34947  sitgaddlemb  35027  eulerpartgbij  35051  eulerpartlemgs2  35059  orvcval  35137  coinfliprv  35162  ballotlemrval  35197  ballotlem7  35215  msrval  36390  mthmval  36427  dfrdg2  36650  tailval  37254  bj-clexab  37970  bj-imdirco  38205  isbasisrelowl  38375  relowlpssretop  38381  lkrval  40239  hashscontpow  43266  imacrhmcl  43675  isnacs3  43815  pw2f1ocnv  44138  pw2f1o2val  44140  lmhmlnmsplit  44183  frege98  45055  frege110  45067  frege133  45090  binomcxplemnotnn0  45434  tgqioo2  46653  smfco  47906  preimafvelsetpreimafv  48564  fundcmpsurinjlem2  48575