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 𝐴 ↔ ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ dom 𝐴 ⊆ dom 𝐴
2	1	biantru	⊢ ( Rel 𝐴 ↔ ( Rel 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴 ) )
3		relssresb	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴 ) ↔ ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )
4	2 3	bitri	⊢ ( Rel 𝐴 ↔ ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )