Theorem funimaex 6594

Description: The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 5217. 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 6593	. 2 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ V) → (𝐴 “ 𝐵) ∈ V)
3	1, 2	mpan2 699	1 ⊢ (Fun 𝐴 → (𝐴 “ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2132  Vcvv 3444   “ cima 5639  Fun wfun 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-rep 5217  ax-sep 5236  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-mo 2556  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-fun 6508

This theorem is referenced by:  isarep2  6596  isofr  7311  isose  7312  f1opw  7637  f1oweALT  7938  ttrclse  9668  tz9.12lem2  9732  hsmexlem4  10372  hsmexlem5  10373  zorn2lem7  10445  uniimadom  10487  zexALT  12574  psdmul  22200  fbasrn  23913  oldf  27896  madefi  27972  negsproplem2  28088  precsexlem10  28275  seqsex  28344  noseqex  28348  zsex  28439  dimval  33842  dimvalfi  33843  onvf1odlem4  35394  onvf1od  35395  fnwe2lem2  43566  relpfr  45468  orbitex  45469  permaxpow  45523  permaxun  45525  permac8prim  45528  setrec2fun  50251