Theorem ssin0

Description: If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	ssin0	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ss2in	⊢ ( ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∩ 𝐵 ) )
2	1	3adant1	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∩ 𝐵 ) )
3		eqimss	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∩ 𝐵 ) ⊆ ∅ )
4	3	3ad2ant1	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ∅ )
5	2 4	sstrd	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ∅ )
6		ss0	⊢ ( ( 𝐶 ∩ 𝐷 ) ⊆ ∅ → ( 𝐶 ∩ 𝐷 ) = ∅ )
7	5 6	syl	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) = ∅ )