Theorem dfdm4

Description: Alternate definition of domain. (Contributed by NM, 28-Dec-1996)

	Ref	Expression
Assertion	dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	1 2	brcnv	$$⊢y{A}^{-1}x\leftrightarrow xAy$$
4	3	exbii	$$⊢\exists yy{A}^{-1}x\leftrightarrow \exists yxAy$$
5	4	abbii	$$⊢\left\{x|\exists yy{A}^{-1}x\right\}=\left\{x|\exists yxAy\right\}$$
6		dfrn2	$$⊢\mathrm{ran}{A}^{-1}=\left\{x|\exists yy{A}^{-1}x\right\}$$
7		df-dm	$$⊢\mathrm{dom}A=\left\{x|\exists yxAy\right\}$$
8	5 6 7	3eqtr4ri	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$