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	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐹 ↾ 𝐵 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( 𝐹 ↾ 𝐵 )
2		reldm0	⊢ ( Rel ( 𝐹 ↾ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) = ∅ ↔ dom ( 𝐹 ↾ 𝐵 ) = ∅ ) )
3	1 2	ax-mp	⊢ ( ( 𝐹 ↾ 𝐵 ) = ∅ ↔ dom ( 𝐹 ↾ 𝐵 ) = ∅ )
4		dmres	⊢ dom ( 𝐹 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
5		incom	⊢ ( 𝐵 ∩ dom 𝐹 ) = ( dom 𝐹 ∩ 𝐵 )
6	4 5	eqtri	⊢ dom ( 𝐹 ↾ 𝐵 ) = ( dom 𝐹 ∩ 𝐵 )
7		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
8	7	ineq1d	⊢ ( 𝐹 Fn 𝐴 → ( dom 𝐹 ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
9	6 8	eqtrid	⊢ ( 𝐹 Fn 𝐴 → dom ( 𝐹 ↾ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
10	9	eqeq1d	⊢ ( 𝐹 Fn 𝐴 → ( dom ( 𝐹 ↾ 𝐵 ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
11	3 10	bitr2id	⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐹 ↾ 𝐵 ) = ∅ ) )