Theorem imaex 7954

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  frxp  8167  frxp2  8185  frxp3  8192  pw2f1o  9143  ssenen  9217  fiint  9394  fiintOLD  9395  fissuni  9427  fipreima  9428  marypha1lem  9502  infxpenlem  10082  ackbij2lem2  10308  enfin2i  10390  fin1a2lem7  10475  fpwwe  10715  canthwelem  10719  tskuni  10852  isacs4lem  18614  gicsubgen  19319  gsumzaddlem  19963  isunit  20399  evpmss  21627  psgnevpmb  21628  ptbasfi  23610  hmphdis  23825  ustuqtop0  24270  utopsnneiplem  24277  neipcfilu  24326  nghmfval  24764  qtopbaslem  24800  fta1glem2  26228  fta1blem  26230  lgsqrlem4  27411  legval  28610  evpmval  33138  altgnsg  33142  elrspunidl  33421  irngval  33685  zarcmplem  33827  brapply  35902  dfrdg4  35915  ptrest  37579  intima0  43610  elintima  43615  brtrclfv2  43689  imaexi  45128  usgrexmpl12ngric  47853