Description: If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | ssin0 | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss2in | ⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∩ 𝐵 ) ) | |
2 | 1 | 3adant1 | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∩ 𝐵 ) ) |
3 | eqimss | ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∩ 𝐵 ) ⊆ ∅ ) | |
4 | 3 | 3ad2ant1 | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ∅ ) |
5 | 2 4 | sstrd | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ∅ ) |
6 | ss0 | ⊢ ( ( 𝐶 ∩ 𝐷 ) ⊆ ∅ → ( 𝐶 ∩ 𝐷 ) = ∅ ) | |
7 | 5 6 | syl | ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) = ∅ ) |