Theorem funimaex 6580

Description: The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 5212. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 17-Nov-2002.)

Hypothesis

Ref	Expression
zfrep5.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
funimaex	⊢ (Fun 𝐴 → (𝐴 “ 𝐵) ∈ V)

Proof of Theorem funimaex

Step	Hyp	Ref	Expression
1		zfrep5.1	. 2 ⊢ 𝐵 ∈ V
2		funimaexg 6579	. 2 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ V) → (𝐴 “ 𝐵) ∈ V)
3	1, 2	mpan2 692	1 ⊢ (Fun 𝐴 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   “ cima 5627  Fun wfun 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494

This theorem is referenced by:  isarep2  6582  isofr  7290  isose  7291  f1opw  7616  f1oweALT  7918  ttrclse  9639  tz9.12lem2  9703  hsmexlem4  10342  hsmexlem5  10343  zorn2lem7  10415  uniimadom  10457  zexALT  12535  psdmul  22142  fbasrn  23859  oldf  27843  madefi  27919  negsproplem2  28035  precsexlem10  28222  seqsex  28291  noseqex  28295  zsex  28386  dimval  33760  dimvalfi  33761  onvf1odlem4  35304  onvf1od  35305  fnwe2lem2  43497  relpfr  45399  orbitex  45400  permaxpow  45454  permaxun  45456  permac8prim  45459  setrec2fun  50179