Description: Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | eldisjss | ⊢ ( 𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴 ) ) |
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 𝐴 ) ) |