Theorem funimaex 3682

Description: The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep 2767. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29.

Hypothesis

Ref	Expression
zfrep5.1	|- B e. V

Assertion

Ref	Expression
funimaex	|- (Fun A -> (A"B) e. V)

Proof of Theorem funimaex

Step	Hyp	Ref	Expression
1		zfrep5.1	. 2 |- B e. V
2		funimaexg 3681	. 2 |- ((Fun A /\ B e. V) -> (A"B) e. V)
3	1, 2	mpan2 700	1 |- (Fun A -> (A"B) e. V)

Syntax hints:   -> wi 3   e. wcel 994  Vcvv 1857  "cima 3254  Fun wfun 3257

This theorem is referenced by:  isarep2 3684  isofrlem 4015  f1oweALT 4020  tz7.44-3 4231  tz9.12lem2 4806  zorn2lem7 4940  uniimadom 4956  ordtypelem7 11433  compfipin0lem 11492  compfipin0 11493  neibastop2lem4 11583  filrn 11643  elfilmap 11690  fmf 11693  fmbas 11694  heiborlem7 12017

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-rex 1696  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-br 2693  df-opab 2741  df-id 2913  df-xp 3265  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273

Copyright terms: Public domain