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	syl5bi	|- ( 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 ) )