Theorem brdomaing

Description: Closed form of brdomain . (Contributed by Scott Fenton, 2-May-2014)

	Ref	Expression
Assertion	brdomaing	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}B\leftrightarrow B=\mathrm{dom}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢a=A\to \left(a\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}b\leftrightarrow A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}b\right)$$
2		dmeq	$$⊢a=A\to \mathrm{dom}a=\mathrm{dom}A$$
3	2	eqeq2d	$$⊢a=A\to \left(b=\mathrm{dom}a\leftrightarrow b=\mathrm{dom}A\right)$$
4	1 3	bibi12d	$$⊢a=A\to \left(\left(a\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}b\leftrightarrow b=\mathrm{dom}a\right)\leftrightarrow \left(A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}b\leftrightarrow b=\mathrm{dom}A\right)\right)$$
5		breq2	$$⊢b=B\to \left(A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}b\leftrightarrow A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}B\right)$$
6		eqeq1	$$⊢b=B\to \left(b=\mathrm{dom}A\leftrightarrow B=\mathrm{dom}A\right)$$
7	5 6	bibi12d	$$⊢b=B\to \left(\left(A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}b\leftrightarrow b=\mathrm{dom}A\right)\leftrightarrow \left(A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}B\leftrightarrow B=\mathrm{dom}A\right)\right)$$
8		vex	$$⊢a\in \mathrm{V}$$
9		vex	$$⊢b\in \mathrm{V}$$
10	8 9	brdomain	$$⊢a\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}b\leftrightarrow b=\mathrm{dom}a$$
11	4 7 10	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{𝖣𝗈𝗆𝖺𝗂𝗇}B\leftrightarrow B=\mathrm{dom}A\right)$$