Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Zhi Wang
ZF Set Theory - start with the Axiom of Extensionality
The empty set
ssdisjdr
Metamath Proof Explorer
Description: Subset preserves disjointness. Deduction form of ssdisj .
Alternatively this could be proved with ineqcom in tandem with
ssdisjd . (Contributed by Zhi Wang , 7-Sep-2024)
Ref
Expression
Hypotheses
ssdisjd.1
⊢ φ → A ⊆ B
ssdisjdr.2
⊢ φ → C ∩ B = ∅
Assertion
ssdisjdr
⊢ φ → C ∩ A = ∅
Proof
Step
Hyp
Ref
Expression
1
ssdisjd.1
⊢ φ → A ⊆ B
2
ssdisjdr.2
⊢ φ → C ∩ B = ∅
3
sslin
⊢ A ⊆ B → C ∩ A ⊆ C ∩ B
4
1 3
syl
⊢ φ → C ∩ A ⊆ C ∩ B
5
sseq0
⊢ C ∩ A ⊆ C ∩ B ∧ C ∩ B = ∅ → C ∩ A = ∅
6
4 2 5
syl2anc
⊢ φ → C ∩ A = ∅