Theorem funimaexg

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)

	Ref	Expression
Assertion	funimaexg	|- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		imaeq2	|- ( w = B -> ( A " w ) = ( A " B ) )
2	1	eleq1d	|- ( w = B -> ( ( A " w ) e. _V <-> ( A " B ) e. _V ) )
3	2	imbi2d	|- ( w = B -> ( ( Fun A -> ( A " w ) e. _V ) <-> ( Fun A -> ( A " B ) e. _V ) ) )
4		dffun5	|- ( Fun A <-> ( Rel A /\ A. x E. z A. y ( <. x , y >. e. A -> y = z ) ) )
5		nfv	|- F/ z <. x , y >. e. A
6	5	axrep4	|- ( A. x E. z A. y ( <. x , y >. e. A -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ <. x , y >. e. A ) ) )
7		isset	|- ( ( A " w ) e. _V <-> E. z z = ( A " w ) )
8		dfima3	|- ( A " w ) = { y | E. x ( x e. w /\ <. x , y >. e. A ) }
9	8	eqeq2i	|- ( z = ( A " w ) <-> z = { y | E. x ( x e. w /\ <. x , y >. e. A ) } )
10		abeq2	|- ( z = { y | E. x ( x e. w /\ <. x , y >. e. A ) } <-> A. y ( y e. z <-> E. x ( x e. w /\ <. x , y >. e. A ) ) )
11	9 10	bitri	|- ( z = ( A " w ) <-> A. y ( y e. z <-> E. x ( x e. w /\ <. x , y >. e. A ) ) )
12	11	exbii	|- ( E. z z = ( A " w ) <-> E. z A. y ( y e. z <-> E. x ( x e. w /\ <. x , y >. e. A ) ) )
13	7 12	bitri	|- ( ( A " w ) e. _V <-> E. z A. y ( y e. z <-> E. x ( x e. w /\ <. x , y >. e. A ) ) )
14	6 13	sylibr	|- ( A. x E. z A. y ( <. x , y >. e. A -> y = z ) -> ( A " w ) e. _V )
15	4 14	simplbiim	|- ( Fun A -> ( A " w ) e. _V )
16	3 15	vtoclg	|- ( B e. C -> ( Fun A -> ( A " B ) e. _V ) )
17	16	impcom	|- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V )