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	⊢ ( 𝜑 → ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )
Assertion	coemptyd	⊢ ( 𝜑 → ( 𝐴 ∘ 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		coemptyd.1	⊢ ( 𝜑 → ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )
2		coeq0	⊢ ( ( 𝐴 ∘ 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )
3	1 2	sylibr	⊢ ( 𝜑 → ( 𝐴 ∘ 𝐵 ) = ∅ )