Theorem reldm

Description: An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013) (Proof shortened by Sky Winter, 22-Oct-2026)

	Ref	Expression
Assertion	reldm	$$⊢\mathrm{Rel}A\to \mathrm{dom}A=\mathrm{ran}\left(x\in A⟼1^{st}\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		releldm2	$$⊢\mathrm{Rel}A\to \left(y\in \mathrm{dom}A\leftrightarrow \exists x\in A{1}^{st}\left(x\right)=y\right)$$
2		eqid	$$⊢\left(x\in A⟼1^{st}\left(x\right)\right)=\left(x\in A⟼1^{st}\left(x\right)\right)$$
3		fvex	$$⊢1^{st}\left(x\right)\in \mathrm{V}$$
4	2 3	elrnmpti	$$⊢y\in \mathrm{ran}\left(x\in A⟼1^{st}\left(x\right)\right)\leftrightarrow \exists x\in Ay=1^{st}\left(x\right)$$
5		eqcom	$$⊢y=1^{st}\left(x\right)\leftrightarrow 1^{st}\left(x\right)=y$$
6	5	rexbii	$$⊢\exists x\in Ay=1^{st}\left(x\right)\leftrightarrow \exists x\in A{1}^{st}\left(x\right)=y$$
7	4 6	bitri	$$⊢y\in \mathrm{ran}\left(x\in A⟼1^{st}\left(x\right)\right)\leftrightarrow \exists x\in A{1}^{st}\left(x\right)=y$$
8	1 7	bitr4di	$$⊢\mathrm{Rel}A\to \left(y\in \mathrm{dom}A\leftrightarrow y\in \mathrm{ran}\left(x\in A⟼1^{st}\left(x\right)\right)\right)$$
9	8	eqrdv	$$⊢\mathrm{Rel}A\to \mathrm{dom}A=\mathrm{ran}\left(x\in A⟼1^{st}\left(x\right)\right)$$