Metamath Proof Explorer

Theorem ssimaexg

Description: The existence of a subimage. (Contributed by FL, 15-Apr-2007)

Ref Expression
Assertion ssimaexg 
|- ( ( A e. C /\ Fun F /\ B C_ ( F " A ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) )

Proof

Step Hyp Ref Expression
1 imaeq2 
 |-  ( y = A -> ( F " y ) = ( F " A ) )
2 1 sseq2d 
 |-  ( y = A -> ( B C_ ( F " y ) <-> B C_ ( F " A ) ) )
3 2 anbi2d 
 |-  ( y = A -> ( ( Fun F /\ B C_ ( F " y ) ) <-> ( Fun F /\ B C_ ( F " A ) ) ) )
4 sseq2 
 |-  ( y = A -> ( x C_ y <-> x C_ A ) )
5 4 anbi1d 
 |-  ( y = A -> ( ( x C_ y /\ B = ( F " x ) ) <-> ( x C_ A /\ B = ( F " x ) ) ) )
6 5 exbidv 
 |-  ( y = A -> ( E. x ( x C_ y /\ B = ( F " x ) ) <-> E. x ( x C_ A /\ B = ( F " x ) ) ) )
7 3 6 imbi12d 
 |-  ( y = A -> ( ( ( Fun F /\ B C_ ( F " y ) ) -> E. x ( x C_ y /\ B = ( F " x ) ) ) <-> ( ( Fun F /\ B C_ ( F " A ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) ) ) )
8 vex 
 |-  y e. _V
9 8 ssimaex 
 |-  ( ( Fun F /\ B C_ ( F " y ) ) -> E. x ( x C_ y /\ B = ( F " x ) ) )
10 7 9 vtoclg 
 |-  ( A e. C -> ( ( Fun F /\ B C_ ( F " A ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) ) )
11 10 3impib 
 |-  ( ( A e. C /\ Fun F /\ B C_ ( F " A ) ) -> E. x ( x C_ A /\ B = ( F " x ) ) )