Theorem dfdm3

Description: Alternate definition of domain. Definition 6.5(1) of TakeutiZaring p. 24. (Contributed by NM, 28-Dec-1996)

	Ref	Expression
Assertion	dfdm3	$$⊢\mathrm{dom}A=\left\{x|\exists y⟨x,y⟩\in A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-dm	$$⊢\mathrm{dom}A=\left\{x|\exists yxAy\right\}$$
2		df-br	$$⊢xAy\leftrightarrow ⟨x,y⟩\in A$$
3	2	exbii	$$⊢\exists yxAy\leftrightarrow \exists y⟨x,y⟩\in A$$
4	3	abbii	$$⊢\left\{x|\exists yxAy\right\}=\left\{x|\exists y⟨x,y⟩\in A\right\}$$
5	1 4	eqtri	$$⊢\mathrm{dom}A=\left\{x|\exists y⟨x,y⟩\in A\right\}$$