Theorem fnimadisj

Description: A class that is disjoint with the domain of a function has an empty image under the function. (Contributed by FL, 24-Jan-2007)

	Ref	Expression
Assertion	fnimadisj	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 “ 𝐶 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
2	1	ineq1d	⊢ ( 𝐹 Fn 𝐴 → ( dom 𝐹 ∩ 𝐶 ) = ( 𝐴 ∩ 𝐶 ) )
3	2	eqeq1d	⊢ ( 𝐹 Fn 𝐴 → ( ( dom 𝐹 ∩ 𝐶 ) = ∅ ↔ ( 𝐴 ∩ 𝐶 ) = ∅ ) )
4	3	biimpar	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( dom 𝐹 ∩ 𝐶 ) = ∅ )
5		imadisj	⊢ ( ( 𝐹 “ 𝐶 ) = ∅ ↔ ( dom 𝐹 ∩ 𝐶 ) = ∅ )
6	4 5	sylibr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐴 ∩ 𝐶 ) = ∅ ) → ( 𝐹 “ 𝐶 ) = ∅ )