Theorem imaexg 7622

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3496   ⊆ wss 3938  ran crn 5558   “ cima 5560

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 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-xp 5563  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570

This theorem is referenced by:  imaex  7623  ecexg  8295  fopwdom  8627  gsumvalx  17888  gsum2dlem1  19092  gsum2dlem2  19093  gsum2d  19094  xkococnlem  22269  qtopval  22305  ustuqtop4  22855  utopsnnei  22860  fmucnd  22903  metustel  23162  metustss  23163  metustfbas  23169  metuel2  23177  psmetutop  23179  restmetu  23182  cnheiborlem  23560  itg2gt0  24363  shsval  29091  nlfnval  29660  fnpreimac  30418  ffsrn  30467  gsummpt2co  30688  gsummpt2d  30689  locfinreflem  31106  qqhval  31217  esum2d  31354  mbfmcnt  31528  sitgaddlemb  31608  eulerpartgbij  31632  eulerpartlemgs2  31640  orvcval  31717  coinfliprv  31742  ballotlemrval  31777  ballotlem7  31795  msrval  32787  mthmval  32824  dfrdg2  33042  tailval  33723  bj-clex  34278  isbasisrelowl  34641  relowlpssretop  34647  lkrval  36226  isnacs3  39314  pw2f1ocnv  39641  pw2f1o2val  39643  lmhmlnmsplit  39694  frege98  40314  frege110  40326  frege133  40349  binomcxplemnotnn0  40695  imaexi  41493  tgqioo2  41830  sge0f1o  42671  smfco  43084  preimafvelsetpreimafv  43555  fundcmpsurinjlem2  43566  isomuspgrlem2a  44000