Theorem imadisj

Description: A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007)

	Ref	Expression
Assertion	imadisj	⊢ ( ( 𝐴 “ 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 )
2	1	eqeq1i	⊢ ( ( 𝐴 “ 𝐵 ) = ∅ ↔ ran ( 𝐴 ↾ 𝐵 ) = ∅ )
3		dm0rn0	⊢ ( dom ( 𝐴 ↾ 𝐵 ) = ∅ ↔ ran ( 𝐴 ↾ 𝐵 ) = ∅ )
4		dmres	⊢ dom ( 𝐴 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐴 )
5		incom	⊢ ( 𝐵 ∩ dom 𝐴 ) = ( dom 𝐴 ∩ 𝐵 )
6	4 5	eqtri	⊢ dom ( 𝐴 ↾ 𝐵 ) = ( dom 𝐴 ∩ 𝐵 )
7	6	eqeq1i	⊢ ( dom ( 𝐴 ↾ 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ 𝐵 ) = ∅ )
8	2 3 7	3bitr2i	⊢ ( ( 𝐴 “ 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ 𝐵 ) = ∅ )