Description: Axiom of Replacement using abbreviations. Axiom 39(vi) of Quine p. 284. Compare Exercise 9 of TakeutiZaring p. 29. (Contributed by NM, 10-Sep-2006) Shorten proof and avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | funimaexg | |- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dffun6 | |- ( Fun A <-> ( Rel A /\ A. x E* y x A y ) ) |
|
| 2 | 1 | simprbi | |- ( Fun A -> A. x E* y x A y ) |
| 3 | dfima2 | |- ( A " B ) = { y | E. x e. B x A y } |
|
| 4 | axrep6g | |- ( ( B e. C /\ A. x E* y x A y ) -> { y | E. x e. B x A y } e. _V ) |
|
| 5 | 3 4 | eqeltrid | |- ( ( B e. C /\ A. x E* y x A y ) -> ( A " B ) e. _V ) |
| 6 | 2 5 | sylan2 | |- ( ( B e. C /\ Fun A ) -> ( A " B ) e. _V ) |
| 7 | 6 | ancoms | |- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V ) |