Theorem imaex 7640

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

Syntax hints:   ∈ wcel 2113  Vcvv 3397   “ cima 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293  ax-un 7473

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by:  frxp  7839  pw2f1o  8664  ssenen  8734  fiint  8862  fissuni  8895  fipreima  8896  marypha1lem  8963  infxpenlem  9506  ackbij2lem2  9733  enfin2i  9814  fin1a2lem7  9899  fpwwe  10139  canthwelem  10143  tskuni  10276  isacs4lem  17887  gicsubgen  18529  gsumzaddlem  19153  isunit  19522  evpmss  20395  psgnevpmb  20396  ptbasfi  22325  hmphdis  22540  ustuqtop0  22985  utopsnneiplem  22992  neipcfilu  23041  nghmfval  23468  qtopbaslem  23504  fta1glem2  24911  fta1blem  24913  lgsqrlem4  26077  legval  26522  evpmval  30981  altgnsg  30985  elrspunidl  31170  zarcmplem  31395  frxp2  33394  frxp3  33400  brapply  33870  dfrdg4  33883  ptrest  35388  intima0  40785  elintima  40791  brtrclfv2  40865