Metamath Proof Explorer


Theorem eldisjssd

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

Ref Expression
Hypothesis eldisjssd.1 ( 𝜑𝐴𝐵 )
Assertion eldisjssd ( 𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eldisjssd.1 ( 𝜑𝐴𝐵 )
2 eldisjss ( 𝐴𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴 ) )
3 1 2 syl ( 𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴 ) )