Theorem fnresdisj

Description: A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004)

	Ref	Expression
Assertion	fnresdisj	|- ( F Fn A -> ( ( A i^i B ) = (/) <-> ( F |` B ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		relres	|- Rel ( F |` B )
2		reldm0	|- ( Rel ( F |` B ) -> ( ( F |` B ) = (/) <-> dom ( F |` B ) = (/) ) )
3	1 2	ax-mp	|- ( ( F |` B ) = (/) <-> dom ( F |` B ) = (/) )
4		dmres	|- dom ( F |` B ) = ( B i^i dom F )
5		incom	|- ( B i^i dom F ) = ( dom F i^i B )
6	4 5	eqtri	|- dom ( F |` B ) = ( dom F i^i B )
7		fndm	|- ( F Fn A -> dom F = A )
8	7	ineq1d	|- ( F Fn A -> ( dom F i^i B ) = ( A i^i B ) )
9	6 8	eqtrid	|- ( F Fn A -> dom ( F |` B ) = ( A i^i B ) )
10	9	eqeq1d	|- ( F Fn A -> ( dom ( F |` B ) = (/) <-> ( A i^i B ) = (/) ) )
11	3 10	bitr2id	|- ( F Fn A -> ( ( A i^i B ) = (/) <-> ( F |` B ) = (/) ) )