Theorem imaex 7903

Description: The image of a set is a set. Theorem 3.17 of [Monk1] p. 39. (Contributed by JJ, 24-Sep-2021.)

Hypothesis

Ref	Expression
imaex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
imaex	⊢ (𝐴 “ 𝐵) ∈ V

Proof of Theorem imaex

Step	Hyp	Ref	Expression
1		imaex.1	. 2 ⊢ 𝐴 ∈ V
2		imaexg 7902	. 2 ⊢ (𝐴 ∈ V → (𝐴 “ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 “ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3474   “ cima 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688

This theorem is referenced by:  frxp  8108  frxp2  8126  frxp3  8133  pw2f1o  9073  ssenen  9147  fiint  9320  fissuni  9353  fipreima  9354  marypha1lem  9424  infxpenlem  10004  ackbij2lem2  10231  enfin2i  10312  fin1a2lem7  10397  fpwwe  10637  canthwelem  10641  tskuni  10774  isacs4lem  18493  gicsubgen  19146  gsumzaddlem  19783  isunit  20179  evpmss  21130  psgnevpmb  21131  ptbasfi  23076  hmphdis  23291  ustuqtop0  23736  utopsnneiplem  23743  neipcfilu  23792  nghmfval  24230  qtopbaslem  24266  fta1glem2  25675  fta1blem  25677  lgsqrlem4  26841  legval  27824  evpmval  32291  altgnsg  32295  elrspunidl  32534  irngval  32737  zarcmplem  32849  brapply  34898  dfrdg4  34911  ptrest  36475  intima0  42384  elintima  42389  brtrclfv2  42463