Metamath Proof Explorer


Theorem ssdisjdr

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 =