Theorem brrange

Description: Binary relation form of the range 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	brrange	$$⊢A\mathrm{𝖱𝖺𝗇𝗀𝖾}B\leftrightarrow B=\mathrm{ran}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({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)B\leftrightarrow B=\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\left[A\right]$$
4		df-range	$$⊢\mathrm{𝖱𝖺𝗇𝗀𝖾}=\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)$$
5	4	breqi	$$⊢A\mathrm{𝖱𝖺𝗇𝗀𝖾}B\leftrightarrow A\mathrm{𝖨𝗆𝖺𝗀𝖾}\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)B$$
6		dfrn5	$$⊢\mathrm{ran}A=\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\left[A\right]$$
7	6	eqeq2i	$$⊢B=\mathrm{ran}A\leftrightarrow B=\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)\left[A\right]$$
8	3 5 7	3bitr4i	$$⊢A\mathrm{𝖱𝖺𝗇𝗀𝖾}B\leftrightarrow B=\mathrm{ran}A$$