Theorem imaex 7893

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   “ cima 5644

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  frxp  8108  frxp2  8126  frxp3  8133  pw2f1o  9051  ssenen  9121  fiint  9284  fiintOLD  9285  fissuni  9315  fipreima  9316  marypha1lem  9391  infxpenlem  9973  ackbij2lem2  10199  enfin2i  10281  fin1a2lem7  10366  fpwwe  10606  canthwelem  10610  tskuni  10743  isacs4lem  18510  gicsubgen  19218  gsumzaddlem  19858  isunit  20289  evpmss  21502  psgnevpmb  21503  ptbasfi  23475  hmphdis  23690  ustuqtop0  24135  utopsnneiplem  24142  neipcfilu  24190  nghmfval  24617  qtopbaslem  24653  fta1glem2  26081  fta1blem  26083  lgsqrlem4  27267  legval  28518  evpmval  33109  altgnsg  33113  elrgspnsubrunlem2  33206  elrspunidl  33406  irngval  33687  zarcmplem  33878  brapply  35933  dfrdg4  35946  ptrest  37620  intima0  43644  elintima  43649  brtrclfv2  43723  imaexi  45222  usgrexmpl12ngric  48033  imasubclem1  49097