Theorem imaex 7854

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438   “ cima 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  frxp  8066  frxp2  8084  frxp3  8091  pw2f1o  9006  ssenen  9075  fiint  9235  fiintOLD  9236  fissuni  9266  fipreima  9267  marypha1lem  9342  infxpenlem  9926  ackbij2lem2  10152  enfin2i  10234  fin1a2lem7  10319  fpwwe  10559  canthwelem  10563  tskuni  10696  isacs4lem  18468  gicsubgen  19176  gsumzaddlem  19818  isunit  20276  evpmss  21511  psgnevpmb  21512  ptbasfi  23484  hmphdis  23699  ustuqtop0  24144  utopsnneiplem  24151  neipcfilu  24199  nghmfval  24626  qtopbaslem  24662  fta1glem2  26090  fta1blem  26092  lgsqrlem4  27276  legval  28547  evpmval  33100  altgnsg  33104  elrgspnsubrunlem2  33201  elrspunidl  33378  irngval  33659  zarcmplem  33850  brapply  35914  dfrdg4  35927  ptrest  37601  intima0  43624  elintima  43629  brtrclfv2  43703  imaexi  45202  usgrexmpl12ngric  48026  imasubclem1  49093