Theorem imaex 7918

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

Syntax hints:   ∈ wcel 2107  Vcvv 3463   “ cima 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  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 4888  df-br 5124  df-opab 5186  df-xp 5671  df-cnv 5673  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678

This theorem is referenced by:  frxp  8133  frxp2  8151  frxp3  8158  pw2f1o  9099  ssenen  9173  fiint  9348  fiintOLD  9349  fissuni  9379  fipreima  9380  marypha1lem  9455  infxpenlem  10035  ackbij2lem2  10261  enfin2i  10343  fin1a2lem7  10428  fpwwe  10668  canthwelem  10672  tskuni  10805  isacs4lem  18559  gicsubgen  19267  gsumzaddlem  19908  isunit  20342  evpmss  21559  psgnevpmb  21560  ptbasfi  23536  hmphdis  23751  ustuqtop0  24196  utopsnneiplem  24203  neipcfilu  24251  nghmfval  24680  qtopbaslem  24716  fta1glem2  26145  fta1blem  26147  lgsqrlem4  27330  legval  28529  evpmval  33109  altgnsg  33113  elrgspnsubrunlem2  33196  elrspunidl  33396  irngval  33677  zarcmplem  33855  brapply  35914  dfrdg4  35927  ptrest  37601  intima0  43638  elintima  43643  brtrclfv2  43717  imaexi  45198  usgrexmpl12ngric  47970