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

Syntax hints:   ∈ wcel 2143  Vcvv 3455   “ cima 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is referenced by:  frxp  8123  frxp2  8141  frxp3  8148  pw2f1o  9071  ssenen  9140  fiint  9287  fissuni  9315  fipreima  9316  marypha1lem  9394  infxpenlem  9998  ackbij2lem2  10223  enfin2i  10306  fin1a2lem7  10391  fpwwe  10632  canthwelem  10636  tskuni  10769  isacs4lem  18601  gicsubgen  19350  gsumzaddlem  19992  isunit  20456  evpmss  21717  psgnevpmb  21718  ptbasfi  23719  hmphdis  23934  ustuqtop0  24378  utopsnneiplem  24385  neipcfilu  24433  nghmfval  24860  qtopbaslem  24896  fta1glem2  26307  fta1blem  26309  lgsqrlem4  27491  legval  28831  evpmval  33443  altgnsg  33447  elrgspnsubrunlem2  33546  elrspunidl  33714  irngval  34053  zarcmplem  34249  brapply  36406  dfrdg4  36421  ptrest  38248  intima0  44354  elintima  44359  brtrclfv2  44433  imaexi  45917  usgrexmpl12ngric  48780  imasubclem1  49859