Theorem funimaex 6608

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   “ cima 5644  Fun wfun 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516

This theorem is referenced by:  isarep2  6611  isofr  7320  isose  7321  f1opw  7648  f1oweALT  7954  ttrclse  9687  tz9.12lem2  9748  hsmexlem4  10389  hsmexlem5  10390  zorn2lem7  10462  uniimadom  10504  zexALT  12556  psdmul  22060  fbasrn  23778  oldf  27772  madefi  27831  negsproplem2  27942  precsexlem10  28125  seqsex  28186  noseqex  28190  zsex  28275  dimval  33603  dimvalfi  33604  onvf1odlem4  35100  onvf1od  35101  fnwe2lem2  43047  relpfr  44951  orbitex  44952  permaxpow  45006  permaxun  45008  permac8prim  45011  setrec2fun  49685