Theorem imaex 7915

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

Syntax hints:   ∈ wcel 2109  Vcvv 3464   “ cima 5662

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

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 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is referenced by:  frxp  8130  frxp2  8148  frxp3  8155  pw2f1o  9096  ssenen  9170  fiint  9343  fiintOLD  9344  fissuni  9374  fipreima  9375  marypha1lem  9450  infxpenlem  10032  ackbij2lem2  10258  enfin2i  10340  fin1a2lem7  10425  fpwwe  10665  canthwelem  10669  tskuni  10802  isacs4lem  18559  gicsubgen  19267  gsumzaddlem  19907  isunit  20338  evpmss  21551  psgnevpmb  21552  ptbasfi  23524  hmphdis  23739  ustuqtop0  24184  utopsnneiplem  24191  neipcfilu  24239  nghmfval  24666  qtopbaslem  24702  fta1glem2  26131  fta1blem  26133  lgsqrlem4  27317  legval  28568  evpmval  33161  altgnsg  33165  elrgspnsubrunlem2  33248  elrspunidl  33448  irngval  33731  zarcmplem  33917  brapply  35961  dfrdg4  35974  ptrest  37648  intima0  43639  elintima  43644  brtrclfv2  43718  imaexi  45212  usgrexmpl12ngric  48009  imasubclem1  49030