This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjssun

Description: Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion disjssun ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 ⊆ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 uneq2 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ∅ ) )
2 indi ⊢ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∩ 𝐶 ) )
3 2 equncomi ⊢ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐴 ∩ 𝐵 ) )
4 un0 ⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ ∅ ) = ( 𝐴 ∩ 𝐶 )
5 4 eqcomi ⊢ ( 𝐴 ∩ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ∅ )
6 1 3 5 3eqtr4g ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐴 ∩ 𝐶 ) )
7 6 eqeq1d ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = 𝐴 ↔ ( 𝐴 ∩ 𝐶 ) = 𝐴 ) )
8 dfss2 ⊢ ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) = 𝐴 )
9 dfss2 ⊢ ( 𝐴 ⊆ 𝐶 ↔ ( 𝐴 ∩ 𝐶 ) = 𝐴 )
10 7 8 9 3bitr4g ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 ⊆ 𝐶 ) )