Theorem imaex 7891

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453   “ cima 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-xp 5651  df-cnv 5653  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658

This theorem is referenced by:  frxp  8101  frxp2  8119  frxp3  8126  pw2f1o  9050  ssenen  9119  fiint  9267  fissuni  9297  fipreima  9298  marypha1lem  9376  infxpenlem  9966  ackbij2lem2  10192  enfin2i  10275  fin1a2lem7  10360  fpwwe  10601  canthwelem  10605  tskuni  10738  isacs4lem  18559  gicsubgen  19302  gsumzaddlem  19944  isunit  20401  evpmss  21618  psgnevpmb  21619  ptbasfi  23621  hmphdis  23836  ustuqtop0  24280  utopsnneiplem  24287  neipcfilu  24335  nghmfval  24762  qtopbaslem  24798  fta1glem2  26209  fta1blem  26211  lgsqrlem4  27390  legval  28730  evpmval  33286  altgnsg  33290  elrgspnsubrunlem2  33390  elrspunidl  33575  irngval  33943  zarcmplem  34139  brapply  36250  dfrdg4  36265  ptrest  38082  intima0  44188  elintima  44193  brtrclfv2  44267  imaexi  45761  usgrexmpl12ngric  48624  imasubclem1  49689