Theorem relssresv

Description: A relation is included in a class if and only if it is included in its "relation part" (see relpart ). (Contributed by BJ, 16-Oct-2026)

	Ref	Expression
Assertion	relssresv	⊢ ( Rel 𝐵 → ( 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ ( 𝐴 ↾ V ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-dfrel3	⊢ ( Rel 𝐵 ↔ ( 𝐵 ↾ V ) = 𝐵 )
2		ssres	⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐵 ↾ V ) ⊆ ( 𝐴 ↾ V ) )
3		sseq1	⊢ ( ( 𝐵 ↾ V ) = 𝐵 → ( ( 𝐵 ↾ V ) ⊆ ( 𝐴 ↾ V ) ↔ 𝐵 ⊆ ( 𝐴 ↾ V ) ) )
4	2 3	imbitrid	⊢ ( ( 𝐵 ↾ V ) = 𝐵 → ( 𝐵 ⊆ 𝐴 → 𝐵 ⊆ ( 𝐴 ↾ V ) ) )
5		id	⊢ ( 𝐵 ⊆ ( 𝐴 ↾ V ) → 𝐵 ⊆ ( 𝐴 ↾ V ) )
6		resss	⊢ ( 𝐴 ↾ V ) ⊆ 𝐴
7	5 6	sstrdi	⊢ ( 𝐵 ⊆ ( 𝐴 ↾ V ) → 𝐵 ⊆ 𝐴 )
8	4 7	impbid1	⊢ ( ( 𝐵 ↾ V ) = 𝐵 → ( 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ ( 𝐴 ↾ V ) ) )
9	1 8	sylbi	⊢ ( Rel 𝐵 → ( 𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ ( 𝐴 ↾ V ) ) )