Description: Subset of restriction, special case. (Contributed by Peter Mazsa, 10-Apr-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | relssinxpdmrn | ⊢ ( Rel 𝑅 → ( 𝑅 ⊆ ( 𝑆 ∩ ( dom 𝑅 × ran 𝑅 ) ) ↔ 𝑅 ⊆ 𝑆 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relssdmrn | ⊢ ( Rel 𝑅 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ) | |
2 | 1 | biantrud | ⊢ ( Rel 𝑅 → ( 𝑅 ⊆ 𝑆 ↔ ( 𝑅 ⊆ 𝑆 ∧ 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ) ) ) |
3 | ssin | ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ) ↔ 𝑅 ⊆ ( 𝑆 ∩ ( dom 𝑅 × ran 𝑅 ) ) ) | |
4 | 2 3 | bitr2di | ⊢ ( Rel 𝑅 → ( 𝑅 ⊆ ( 𝑆 ∩ ( dom 𝑅 × ran 𝑅 ) ) ↔ 𝑅 ⊆ 𝑆 ) ) |