Theorem imaexg 7384

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 5733	. 2 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴
2		rnexg 7378	. 2 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
3		ssexg 5043	. 2 ⊢ (((𝐴 “ 𝐵) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V) → (𝐴 “ 𝐵) ∈ V)
4	1, 2, 3	sylancr 581	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3398   ⊆ wss 3792  ran crn 5358   “ cima 5360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140  ax-un 7228

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-xp 5363  df-cnv 5365  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370

This theorem is referenced by:  imaex  7385  ecexg  8032  fopwdom  8358  gsumvalx  17660  gsum2dlem1  18759  gsum2dlem2  18760  gsum2d  18761  xkococnlem  21875  qtopval  21911  ustuqtop4  22460  utopsnnei  22465  fmucnd  22508  metustel  22767  metustss  22768  metustfbas  22774  metuel2  22782  psmetutop  22784  restmetu  22787  cnheiborlem  23165  itg2gt0  23968  shsval  28747  nlfnval  29316  fnpreimac  30040  ffsrn  30074  gsummpt2co  30346  gsummpt2d  30347  locfinreflem  30509  qqhval  30620  esum2d  30757  mbfmcnt  30932  sitgaddlemb  31012  eulerpartgbij  31036  eulerpartlemgs2  31044  orvcval  31122  coinfliprv  31147  ballotlemrval  31182  ballotlem7  31200  msrval  32038  mthmval  32075  dfrdg2  32293  tailval  32960  bj-clex  33528  isbasisrelowl  33804  relowlpssretop  33810  ptrest  34039  lkrval  35247  isnacs3  38243  pw2f1ocnv  38573  pw2f1o2val  38575  lmhmlnmsplit  38626  intima0  38906  elintima  38912  brtrclfv2  38986  frege98  39221  frege110  39233  frege133  39256  binomcxplemnotnn0  39521  imaexi  40346  tgqioo2  40692  sge0f1o  41533  smfco  41946  isomuspgrlem2a  42751