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 𝐴 ) )