Theorem imaex 7856

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440   “ cima 5627

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  frxp  8068  frxp2  8086  frxp3  8093  pw2f1o  9010  ssenen  9079  fiint  9227  fissuni  9257  fipreima  9258  marypha1lem  9336  infxpenlem  9923  ackbij2lem2  10149  enfin2i  10231  fin1a2lem7  10316  fpwwe  10557  canthwelem  10561  tskuni  10694  isacs4lem  18467  gicsubgen  19208  gsumzaddlem  19850  isunit  20309  evpmss  21541  psgnevpmb  21542  ptbasfi  23525  hmphdis  23740  ustuqtop0  24184  utopsnneiplem  24191  neipcfilu  24239  nghmfval  24666  qtopbaslem  24702  fta1glem2  26130  fta1blem  26132  lgsqrlem4  27316  legval  28656  evpmval  33227  altgnsg  33231  elrgspnsubrunlem2  33330  elrspunidl  33509  irngval  33842  zarcmplem  34038  brapply  36130  dfrdg4  36145  ptrest  37816  intima0  43885  elintima  43890  brtrclfv2  43964  imaexi  45461  usgrexmpl12ngric  48280  imasubclem1  49345