This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eldisjss

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

Ref Expression
Assertion eldisjss ⊢ A ⊆ B → ElDisj B → ElDisj A

Proof

Step Hyp Ref Expression
1 ssres2 ⊢ A ⊆ B → E -1 ↾ A ⊆ E -1 ↾ B
2 1 disjssd ⊢ A ⊆ B → Disj E -1 ↾ B → Disj E -1 ↾ A
3 df-eldisj ⊢ ElDisj B ↔ Disj E -1 ↾ B
4 df-eldisj ⊢ ElDisj A ↔ Disj E -1 ↾ A
5 2 3 4 3imtr4g ⊢ A ⊆ B → ElDisj B → ElDisj A