Theorem coemptyd

Description: Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypothesis	coemptyd.1	|- ( ph -> ( dom A i^i ran B ) = (/) )
Assertion	coemptyd	|- ( ph -> ( A o. B ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		coemptyd.1	|- ( ph -> ( dom A i^i ran B ) = (/) )
2		coeq0	|- ( ( A o. B ) = (/) <-> ( dom A i^i ran B ) = (/) )
3	1 2	sylibr	|- ( ph -> ( A o. B ) = (/) )