Theorem relssdmrnOLD

Description: Obsolete version of relssdmrn as of 23-Dec-2024. (Contributed by NM, 3-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	relssdmrnOLD	$$⊢\mathrm{Rel}A\to A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\mathrm{Rel}A\to \mathrm{Rel}A$$
2		19.8a	$$⊢⟨x,y⟩\in A\to \exists y⟨x,y⟩\in A$$
3		19.8a	$$⊢⟨x,y⟩\in A\to \exists x⟨x,y⟩\in A$$
4		opelxp	$$⊢⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)\leftrightarrow \left(x\in \mathrm{dom}A\wedge y\in \mathrm{ran}A\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	eldm2	$$⊢x\in \mathrm{dom}A\leftrightarrow \exists y⟨x,y⟩\in A$$
7		vex	$$⊢y\in \mathrm{V}$$
8	7	elrn2	$$⊢y\in \mathrm{ran}A\leftrightarrow \exists x⟨x,y⟩\in A$$
9	6 8	anbi12i	$$⊢\left(x\in \mathrm{dom}A\wedge y\in \mathrm{ran}A\right)\leftrightarrow \left(\exists y⟨x,y⟩\in A\wedge \exists x⟨x,y⟩\in A\right)$$
10	4 9	bitri	$$⊢⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)\leftrightarrow \left(\exists y⟨x,y⟩\in A\wedge \exists x⟨x,y⟩\in A\right)$$
11	2 3 10	sylanbrc	$$⊢⟨x,y⟩\in A\to ⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)$$
12	11	a1i	$$⊢\mathrm{Rel}A\to \left(⟨x,y⟩\in A\to ⟨x,y⟩\in \left(\mathrm{dom}A\times \mathrm{ran}A\right)\right)$$
13	1 12	relssdv	$$⊢\mathrm{Rel}A\to A\subseteq \mathrm{dom}A\times \mathrm{ran}A$$