Theorem imaex 7844

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   “ cima 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-xp 5622  df-cnv 5624  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629

This theorem is referenced by:  frxp  8056  frxp2  8074  frxp3  8081  pw2f1o  8995  ssenen  9064  fiint  9211  fissuni  9241  fipreima  9242  marypha1lem  9317  infxpenlem  9904  ackbij2lem2  10130  enfin2i  10212  fin1a2lem7  10297  fpwwe  10537  canthwelem  10541  tskuni  10674  isacs4lem  18450  gicsubgen  19192  gsumzaddlem  19834  isunit  20292  evpmss  21524  psgnevpmb  21525  ptbasfi  23497  hmphdis  23712  ustuqtop0  24156  utopsnneiplem  24163  neipcfilu  24211  nghmfval  24638  qtopbaslem  24674  fta1glem2  26102  fta1blem  26104  lgsqrlem4  27288  legval  28563  evpmval  33112  altgnsg  33116  elrgspnsubrunlem2  33213  elrspunidl  33391  irngval  33696  zarcmplem  33892  brapply  35978  dfrdg4  35991  ptrest  37665  intima0  43687  elintima  43692  brtrclfv2  43766  imaexi  45264  usgrexmpl12ngric  48075  imasubclem1  49142