Metamath Proof Explorer

Theorem funimass3

Description: A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv would be the special case of A being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion funimass3 
|- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )

Proof

Step Hyp Ref Expression
1 funimass4 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )
2 ssel 
 |-  ( A C_ dom F -> ( x e. A -> x e. dom F ) )
3 fvimacnv 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) e. B <-> x e. ( `' F " B ) ) )
4 3 ex 
 |-  ( Fun F -> ( x e. dom F -> ( ( F ` x ) e. B <-> x e. ( `' F " B ) ) ) )
5 2 4 syl9r 
 |-  ( Fun F -> ( A C_ dom F -> ( x e. A -> ( ( F ` x ) e. B <-> x e. ( `' F " B ) ) ) ) )
6 5 imp31 
 |-  ( ( ( Fun F /\ A C_ dom F ) /\ x e. A ) -> ( ( F ` x ) e. B <-> x e. ( `' F " B ) ) )
7 6 ralbidva 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( A. x e. A ( F ` x ) e. B <-> A. x e. A x e. ( `' F " B ) ) )
8 1 7 bitrd 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A x e. ( `' F " B ) ) )
9 dfss3 
 |-  ( A C_ ( `' F " B ) <-> A. x e. A x e. ( `' F " B ) )
10 8 9 bitr4di 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )