Metamath Proof Explorer


Theorem relssinxpdmrn

Description: Subset of restriction, special case. (Contributed by Peter Mazsa, 10-Apr-2023)

Ref Expression
Assertion relssinxpdmrn ( Rel 𝑅 → ( 𝑅 ⊆ ( 𝑆 ∩ ( dom 𝑅 × ran 𝑅 ) ) ↔ 𝑅𝑆 ) )

Proof

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 𝑅 ) ) ↔ 𝑅𝑆 ) )