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
|- ( 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 ) = (/) )