Theorem fint

Description: Function into an intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Hypothesis	fint.1	|- B =/= (/)
Assertion	fint	|- ( F : A --> |^| B <-> A. x e. B F : A --> x )

Proof

Step	Hyp	Ref	Expression
1		fint.1	|- B =/= (/)
2		ssint	|- ( ran F C_ |^| B <-> A. x e. B ran F C_ x )
3	2	anbi2i	|- ( ( F Fn A /\ ran F C_ |^| B ) <-> ( F Fn A /\ A. x e. B ran F C_ x ) )
4		r19.28zv	|- ( B =/= (/) -> ( A. x e. B ( F Fn A /\ ran F C_ x ) <-> ( F Fn A /\ A. x e. B ran F C_ x ) ) )
5	1 4	ax-mp	|- ( A. x e. B ( F Fn A /\ ran F C_ x ) <-> ( F Fn A /\ A. x e. B ran F C_ x ) )
6	3 5	bitr4i	|- ( ( F Fn A /\ ran F C_ |^| B ) <-> A. x e. B ( F Fn A /\ ran F C_ x ) )
7		df-f	|- ( F : A --> |^| B <-> ( F Fn A /\ ran F C_ |^| B ) )
8		df-f	|- ( F : A --> x <-> ( F Fn A /\ ran F C_ x ) )
9	8	ralbii	|- ( A. x e. B F : A --> x <-> A. x e. B ( F Fn A /\ ran F C_ x ) )
10	6 7 9	3bitr4i	|- ( F : A --> |^| B <-> A. x e. B F : A --> x )