Theorem imaex 7915

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   “ cima 5654

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 2733  ax-sep 5249  ax-pr 5391  ax-un 7740

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  frxp  8127  frxp2  8145  frxp3  8152  pw2f1o  9085  ssenen  9154  fiint  9302  fissuni  9330  fipreima  9331  marypha1lem  9409  infxpenlem  10073  ackbij2lem2  10298  enfin2i  10380  fin1a2lem7  10465  fpwwe  10712  canthwelem  10716  tskuni  10849  isacs4lem  18698  gicsubgen  19473  gsumzaddlem  20115  isunit  20583  evpmss  21872  psgnevpmb  21873  ptbasfi  23880  hmphdis  24095  ustuqtop0  24539  utopsnneiplem  24546  neipcfilu  24594  nghmfval  25021  qtopbaslem  25057  fta1glem2  26467  fta1blem  26469  lgsqrlem4  27658  legval  29029  evpmval  33688  altgnsg  33692  elrgspnsubrunlem2  33791  elrspunidl  33960  irngval  34299  zarcmplem  34495  brapply  36670  dfrdg4  36685  ptrest  38505  intima0  44607  elintima  44612  brtrclfv2  44686  imaexi  46177  usgrexmpl12ngric  49080  imasubclem1  50156