Description: A restricted class is included in a class if and only if it is included in that class restricted to any class including the first restricting class. (Contributed by BJ, 25-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | resssres | ⊢ ( 𝑋 ⊆ 𝑌 → ( ( 𝐴 ↾ 𝑋 ) ⊆ 𝐵 ↔ ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑌 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssres | ⊢ ( ( 𝐴 ↾ 𝑋 ) ⊆ 𝐵 → ( ( 𝐴 ↾ 𝑋 ) ↾ 𝑌 ) ⊆ ( 𝐵 ↾ 𝑌 ) ) | |
| 2 | resabs2 | ⊢ ( 𝑋 ⊆ 𝑌 → ( ( 𝐴 ↾ 𝑋 ) ↾ 𝑌 ) = ( 𝐴 ↾ 𝑋 ) ) | |
| 3 | 2 | sseq1d | ⊢ ( 𝑋 ⊆ 𝑌 → ( ( ( 𝐴 ↾ 𝑋 ) ↾ 𝑌 ) ⊆ ( 𝐵 ↾ 𝑌 ) ↔ ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑌 ) ) ) |
| 4 | 1 3 | imbitrid | ⊢ ( 𝑋 ⊆ 𝑌 → ( ( 𝐴 ↾ 𝑋 ) ⊆ 𝐵 → ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑌 ) ) ) |
| 5 | id | ⊢ ( ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑌 ) → ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑌 ) ) | |
| 6 | resss | ⊢ ( 𝐵 ↾ 𝑌 ) ⊆ 𝐵 | |
| 7 | 5 6 | sstrdi | ⊢ ( ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑌 ) → ( 𝐴 ↾ 𝑋 ) ⊆ 𝐵 ) |
| 8 | 4 7 | impbid1 | ⊢ ( 𝑋 ⊆ 𝑌 → ( ( 𝐴 ↾ 𝑋 ) ⊆ 𝐵 ↔ ( 𝐴 ↾ 𝑋 ) ⊆ ( 𝐵 ↾ 𝑌 ) ) ) |