Theorem imaex 7763

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 7762	. 2 ⊢ (𝐴 ∈ V → (𝐴 “ 𝐵) ∈ V)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 “ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3432   “ cima 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602

This theorem is referenced by:  frxp  7967  pw2f1o  8864  ssenen  8938  fiint  9091  fissuni  9124  fipreima  9125  marypha1lem  9192  infxpenlem  9769  ackbij2lem2  9996  enfin2i  10077  fin1a2lem7  10162  fpwwe  10402  canthwelem  10406  tskuni  10539  isacs4lem  18262  gicsubgen  18894  gsumzaddlem  19522  isunit  19899  evpmss  20791  psgnevpmb  20792  ptbasfi  22732  hmphdis  22947  ustuqtop0  23392  utopsnneiplem  23399  neipcfilu  23448  nghmfval  23886  qtopbaslem  23922  fta1glem2  25331  fta1blem  25333  lgsqrlem4  26497  legval  26945  evpmval  31412  altgnsg  31416  elrspunidl  31606  zarcmplem  31831  frxp2  33791  frxp3  33797  brapply  34240  dfrdg4  34253  ptrest  35776  intima0  41256  elintima  41261  brtrclfv2  41335