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 A <-> A C_ ( dom A X. ran A ) )

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	|- ( Rel A -> A C_ ( dom A X. ran A ) )
2		id	|- ( A C_ ( dom A X. ran A ) -> A C_ ( dom A X. ran A ) )
3		xpss	|- ( dom A X. ran A ) C_ ( _V X. _V )
4	2 3	sstrdi	|- ( A C_ ( dom A X. ran A ) -> A C_ ( _V X. _V ) )
5		df-rel	|- ( Rel A <-> A C_ ( _V X. _V ) )
6	4 5	sylibr	|- ( A C_ ( dom A X. ran A ) -> Rel A )
7	1 6	impbii	|- ( Rel A <-> A C_ ( dom A X. ran A ) )