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	|- ( ( A " B ) = (/) <-> ( dom A i^i B ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-ima	|- ( A " B ) = ran ( A |` B )
2	1	eqeq1i	|- ( ( A " B ) = (/) <-> ran ( A |` B ) = (/) )
3		dm0rn0	|- ( dom ( A |` B ) = (/) <-> ran ( A |` B ) = (/) )
4		dmres	|- dom ( A |` B ) = ( B i^i dom A )
5		incom	|- ( B i^i dom A ) = ( dom A i^i B )
6	4 5	eqtri	|- dom ( A |` B ) = ( dom A i^i B )
7	6	eqeq1i	|- ( dom ( A |` B ) = (/) <-> ( dom A i^i B ) = (/) )
8	2 3 7	3bitr2i	|- ( ( A " B ) = (/) <-> ( dom A i^i B ) = (/) )