Theorem relssresb

Description: Biconditional form of relssres , to replace it. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	relssresb	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵 ) ↔ ( 𝐴 ↾ 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		relssdmrnb	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )
2		simpl	⊢ ( ( 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) ∧ dom 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )
3		simpr	⊢ ( ( 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) ∧ dom 𝐴 ⊆ 𝐵 ) → dom 𝐴 ⊆ 𝐵 )
4		ssv	⊢ ran 𝐴 ⊆ V
5		xpss12	⊢ ( ( dom 𝐴 ⊆ 𝐵 ∧ ran 𝐴 ⊆ V ) → ( dom 𝐴 × ran 𝐴 ) ⊆ ( 𝐵 × V ) )
6	3 4 5	sylancl	⊢ ( ( 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) ∧ dom 𝐴 ⊆ 𝐵 ) → ( dom 𝐴 × ran 𝐴 ) ⊆ ( 𝐵 × V ) )
7	2 6	sstrd	⊢ ( ( 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) ∧ dom 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ ( 𝐵 × V ) )
8	1 7	sylanb	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ ( 𝐵 × V ) )
9		id	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → 𝐴 ⊆ ( 𝐵 × V ) )
10		xpss	⊢ ( 𝐵 × V ) ⊆ ( V × V )
11	9 10	sstrdi	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → 𝐴 ⊆ ( V × V ) )
12		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
13	11 12	sylibr	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → Rel 𝐴 )
14		dmss	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → dom 𝐴 ⊆ dom ( 𝐵 × V ) )
15		dmxpss	⊢ dom ( 𝐵 × V ) ⊆ 𝐵
16	14 15	sstrdi	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → dom 𝐴 ⊆ 𝐵 )
17	13 16	jca	⊢ ( 𝐴 ⊆ ( 𝐵 × V ) → ( Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵 ) )
18	8 17	impbii	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵 ) ↔ 𝐴 ⊆ ( 𝐵 × V ) )
19		bj-resssxp	⊢ ( ( 𝐴 ↾ 𝐵 ) = 𝐴 ↔ 𝐴 ⊆ ( 𝐵 × V ) )
20	18 19	bitr4i	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐵 ) ↔ ( 𝐴 ↾ 𝐵 ) = 𝐴 )