Metamath Proof Explorer
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 |
⊢ ( 𝜑 → ( 𝐴 ∘ 𝐵 ) = ∅ ) |