Theorem relssdmrnb

Description: Biconditional form of relssdmrn , to replace it. (Contributed by BJ, 8-Nov-2026) TODO: prove dfres3 from it.

	Ref	Expression
Assertion	relssdmrnb	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	⊢ ( Rel 𝐴 → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )
2		id	⊢ ( 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )
3		xpss	⊢ ( dom 𝐴 × ran 𝐴 ) ⊆ ( V × V )
4	2 3	sstrdi	⊢ ( 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) → 𝐴 ⊆ ( V × V ) )
5		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
6	4 5	sylibr	⊢ ( 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) → Rel 𝐴 )
7	1 6	impbii	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )