Theorem imaex 7912

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450   “ cima 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  frxp  8125  frxp2  8143  frxp3  8150  pw2f1o  9083  ssenen  9152  fiint  9299  fissuni  9327  fipreima  9328  marypha1lem  9406  infxpenlem  10019  ackbij2lem2  10244  enfin2i  10326  fin1a2lem7  10411  fpwwe  10658  canthwelem  10662  tskuni  10795  isacs4lem  18635  gicsubgen  19409  gsumzaddlem  20051  isunit  20517  evpmss  21802  psgnevpmb  21803  ptbasfi  23810  hmphdis  24025  ustuqtop0  24469  utopsnneiplem  24476  neipcfilu  24524  nghmfval  24951  qtopbaslem  24987  fta1glem2  26397  fta1blem  26399  lgsqrlem4  27588  legval  28929  evpmval  33588  altgnsg  33592  elrgspnsubrunlem2  33691  elrspunidl  33859  irngval  34198  zarcmplem  34394  brapply  36518  dfrdg4  36533  ptrest  38371  intima0  44491  elintima  44496  brtrclfv2  44570  imaexi  46054  usgrexmpl12ngric  48957  imasubclem1  50033