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	$$⊢\phi \to \mathrm{dom}A\cap \mathrm{ran}B=\varnothing$$
Assertion	coemptyd	$$⊢\phi \to A\circ B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		coemptyd.1	$$⊢\phi \to \mathrm{dom}A\cap \mathrm{ran}B=\varnothing$$
2		coeq0	$$⊢A\circ B=\varnothing \leftrightarrow \mathrm{dom}A\cap \mathrm{ran}B=\varnothing$$
3	1 2	sylibr	$$⊢\phi \to A\circ B=\varnothing$$