Metamath Proof Explorer

Theorem funimaexgOLD

Description: Obsolete version of funimaexg as of 19-Dec-2024. (Contributed by NM, 10-Sep-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion funimaexgOLD 
|- ( ( 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 eqabb 
 |-  ( 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 )