Theorem imaexg 7919

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458   ⊆ wss 3908  ran crn 5667   “ cima 5669

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679

This theorem is used by:  imaex  7920  imaexd  7922  ecexg  8707  fopwdom  9083  gsumvalx  18763  gsum2dlem1  20071  gsum2dlem2  20072  gsum2d  20073  xkococnlem  23853  qtopval  23889  ustuqtop4  24438  utopsnnei  24443  fmucnd  24485  metustel  24744  metustss  24745  metustfbas  24751  metuel2  24759  psmetutop  24761  restmetu  24764  cnheiborlem  25150  itg2gt0  25956  shsval  31701  nlfnval  32270  fnpreimac  33052  ffsrn  33110  pwrssmgc  33351  gsummpt2co  33399  gsummpt2d  33400  qusima  33748  elrspunidl  33767  ply1degltdimlem  34043  algextdeglem8  34145  locfinreflem  34261  zarcmplem  34302  rhmpreimacnlem  34305  qqhval  34393  esum2d  34514  mbfmcnt  34690  sitgaddlemb  34770  eulerpartgbij  34794  eulerpartlemgs2  34802  orvcval  34880  coinfliprv  34905  ballotlemrval  34940  ballotlem7  34958  msrval  36051  mthmval  36088  dfrdg2  36306  tailval  36925  bj-clexab  37641  bj-imdirco  37875  isbasisrelowl  38045  relowlpssretop  38051  lkrval  39903  hashscontpow  42930  imacrhmcl  43329  isnacs3  43482  pw2f1ocnv  43805  pw2f1o2val  43807  lmhmlnmsplit  43855  frege98  44728  frege110  44740  frege133  44763  binomcxplemnotnn0  45107  tgqioo2  46304  smfco  47557  preimafvelsetpreimafv  48178  fundcmpsurinjlem2  48189