Theorem brdomain

Description: Binary relation form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brdomain.1	$$⊢A\in \mathrm{V}$$
	brdomain.2	$$⊢B\in \mathrm{V}$$
Assertion	brdomain	$$⊢A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}B\leftrightarrow B=\mathrm{dom}A$$

Proof

Step	Hyp	Ref	Expression
1		brdomain.1	$$⊢A\in \mathrm{V}$$
2		brdomain.2	$$⊢B\in \mathrm{V}$$
3	1 2	brimage	$$⊢A\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)B\leftrightarrow B=\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\left[A\right]$$
4		df-domain	$$⊢\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
5	4	breqi	$$⊢A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}B\leftrightarrow A\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)B$$
6		dfdm5	$$⊢\mathrm{dom}A=\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\left[A\right]$$
7	6	eqeq2i	$$⊢B=\mathrm{dom}A\leftrightarrow B=\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\left[A\right]$$
8	3 5 7	3bitr4i	$$⊢A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}B\leftrightarrow B=\mathrm{dom}A$$