Description: The image of a set under any function is also a set. Equivalent of Axiom of Replacement ax-rep . Axiom 39(vi) of Quine p. 284. Compare Exercise 9 of TakeutiZaring p. 29. (Contributed by NM, 17-Nov-2002)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | zfrep5.1 | |- B e. _V |
|
| Assertion | funimaex | |- ( Fun A -> ( A " B ) e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zfrep5.1 | |- B e. _V |
|
| 2 | funimaexg | |- ( ( Fun A /\ B e. _V ) -> ( A " B ) e. _V ) |
|
| 3 | 1 2 | mpan2 | |- ( Fun A -> ( A " B ) e. _V ) |