Theorem dfbigcup2

Description: Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	dfbigcup2	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}=\left(x\in \mathrm{V}⟼\bigcup x\right)$$

Proof

Step	Hyp	Ref	Expression
1		relbigcup	$$⊢\mathrm{Rel}\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}$$
2		mptrel	$$⊢\mathrm{Rel}\left(x\in \mathrm{V}⟼\bigcup x\right)$$
3		eqcom	$$⊢\bigcup y=z\leftrightarrow z=\bigcup y$$
4		vex	$$⊢z\in \mathrm{V}$$
5	4	brbigcup	$$⊢y\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}z\leftrightarrow \bigcup y=z$$
6		vex	$$⊢y\in \mathrm{V}$$
7		eleq1w	$$⊢x=y\to \left(x\in \mathrm{V}\leftrightarrow y\in \mathrm{V}\right)$$
8		unieq	$$⊢x=y\to \bigcup x=\bigcup y$$
9	8	eqeq2d	$$⊢x=y\to \left(t=\bigcup x\leftrightarrow t=\bigcup y\right)$$
10	7 9	anbi12d	$$⊢x=y\to \left(\left(x\in \mathrm{V}\wedge t=\bigcup x\right)\leftrightarrow \left(y\in \mathrm{V}\wedge t=\bigcup y\right)\right)$$
11	6	biantrur	$$⊢t=\bigcup y\leftrightarrow \left(y\in \mathrm{V}\wedge t=\bigcup y\right)$$
12	10 11	bitr4di	$$⊢x=y\to \left(\left(x\in \mathrm{V}\wedge t=\bigcup x\right)\leftrightarrow t=\bigcup y\right)$$
13		eqeq1	$$⊢t=z\to \left(t=\bigcup y\leftrightarrow z=\bigcup y\right)$$
14		df-mpt	$$⊢\left(x\in \mathrm{V}⟼\bigcup x\right)=\left\{⟨x,t⟩|\left(x\in \mathrm{V}\wedge t=\bigcup x\right)\right\}$$
15	6 4 12 13 14	brab	$$⊢y\left(x\in \mathrm{V}⟼\bigcup x\right)z\leftrightarrow z=\bigcup y$$
16	3 5 15	3bitr4i	$$⊢y\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}z\leftrightarrow y\left(x\in \mathrm{V}⟼\bigcup x\right)z$$
17	1 2 16	eqbrriv	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}=\left(x\in \mathrm{V}⟼\bigcup x\right)$$