Metamath Proof Explorer


Theorem eldisjss

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

Ref Expression
Assertion eldisjss ( 𝐴𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ssres2 ( 𝐴𝐵 → ( E ↾ 𝐴 ) ⊆ ( E ↾ 𝐵 ) )
2 1 disjssd ( 𝐴𝐵 → ( Disj ( E ↾ 𝐵 ) → Disj ( E ↾ 𝐴 ) ) )
3 df-eldisj ( ElDisj 𝐵 ↔ Disj ( E ↾ 𝐵 ) )
4 df-eldisj ( ElDisj 𝐴 ↔ Disj ( E ↾ 𝐴 ) )
5 2 3 4 3imtr4g ( 𝐴𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴 ) )