Theorem resdmb

Description: Biconditional form of resdm , to replace it. (Contributed by BJ, 8-Nov-2026) TODO: this is dfrel5 : move to main section and update credits.

	Ref	Expression
Assertion	resdmb	|- ( Rel A <-> ( A |` dom A ) = A )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- dom A C_ dom A
2	1	biantru	|- ( Rel A <-> ( Rel A /\ dom A C_ dom A ) )
3		relssresb	|- ( ( Rel A /\ dom A C_ dom A ) <-> ( A |` dom A ) = A )
4	2 3	bitri	|- ( Rel A <-> ( A |` dom A ) = A )