Metamath Proof Explorer

Theorem disjssi

Description: Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021)

Ref Expression
Hypothesis disjssi.1 
|- A C_ B
Assertion disjssi 
|- ( Disj B -> Disj A )

Proof

Step Hyp Ref Expression
1 disjssi.1 
 |-  A C_ B
2 disjss 
 |-  ( A C_ B -> ( Disj B -> Disj A ) )
3 1 2 ax-mp 
 |-  ( Disj B -> Disj A )