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	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	$$⊢\mathrm{Rel}A\to A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
2		id	$$⊢A\subseteq \mathrm{dom}A\times \mathrm{ran}A\to A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$
3		xpss	$$⊢\mathrm{dom}A\times \mathrm{ran}A\subseteq \mathrm{V}\times \mathrm{V}$$
4	2 3	sstrdi	$$⊢A\subseteq \mathrm{dom}A\times \mathrm{ran}A\to A\subseteq \mathrm{V}\times \mathrm{V}$$
5		df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$
6	4 5	sylibr	$$⊢A\subseteq \mathrm{dom}A\times \mathrm{ran}A\to \mathrm{Rel}A$$
7	1 6	impbii	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$