This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dff4

Description: Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion dff4 
|- ( F : A --> B <-> ( F C_ ( A X. B ) /\ A. x e. A E! y e. B x F y ) )

Proof

Step Hyp Ref Expression
1 dff3 
 |-  ( F : A --> B <-> ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) )
2 df-br 
 |-  ( x F y <-> <. x , y >. e. F )
3 ssel 
 |-  ( F C_ ( A X. B ) -> ( <. x , y >. e. F -> <. x , y >. e. ( A X. B ) ) )
4 opelxp2 
 |-  ( <. x , y >. e. ( A X. B ) -> y e. B )
5 3 4 syl6 
 |-  ( F C_ ( A X. B ) -> ( <. x , y >. e. F -> y e. B ) )
6 2 5 biimtrid 
 |-  ( F C_ ( A X. B ) -> ( x F y -> y e. B ) )
7 6 pm4.71rd 
 |-  ( F C_ ( A X. B ) -> ( x F y <-> ( y e. B /\ x F y ) ) )
8 7 eubidv 
 |-  ( F C_ ( A X. B ) -> ( E! y x F y <-> E! y ( y e. B /\ x F y ) ) )
9 df-reu 
 |-  ( E! y e. B x F y <-> E! y ( y e. B /\ x F y ) )
10 8 9 bitr4di 
 |-  ( F C_ ( A X. B ) -> ( E! y x F y <-> E! y e. B x F y ) )
11 10 ralbidv 
 |-  ( F C_ ( A X. B ) -> ( A. x e. A E! y x F y <-> A. x e. A E! y e. B x F y ) )
12 11 pm5.32i 
 |-  ( ( F C_ ( A X. B ) /\ A. x e. A E! y x F y ) <-> ( F C_ ( A X. B ) /\ A. x e. A E! y e. B x F y ) )
13 1 12 bitri 
 |-  ( F : A --> B <-> ( F C_ ( A X. B ) /\ A. x e. A E! y e. B x F y ) )