This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to dom A \cap ran B = \emptyset$
	Assertion	coemptyd	$⊢ φ \to A \circ B = \emptyset$

Step	Hyp	Ref	Expression
1		coemptyd.1	$⊢ φ \to dom A \cap ran B = \emptyset$
2		coeq0	$⊢ A \circ B = \emptyset \leftrightarrow dom A \cap ran B = \emptyset$
3	1 2	sylibr	$⊢ φ \to A \circ B = \emptyset$