Metamath Proof Explorer

Theorem eldisjssi

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

Ref Expression
Hypothesis eldisjssi.1 
|- A C_ B
Assertion eldisjssi 
|- ( ElDisj B -> ElDisj A )

Proof

Step Hyp Ref Expression
1 eldisjssi.1 
 |-  A C_ B
2 eldisjss 
 |-  ( A C_ B -> ( ElDisj B -> ElDisj A ) )
3 1 2 ax-mp 
 |-  ( ElDisj B -> ElDisj A )