Theorem fvbigcup

Description: For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Hypothesis	fvbigcup.1	$$⊢A\in \mathrm{V}$$
Assertion	fvbigcup	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\left(A\right)=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		fvbigcup.1	$$⊢A\in \mathrm{V}$$
2		eqid	$$⊢\bigcup A=\bigcup A$$
3	1	uniex	$$⊢\bigcup A\in \mathrm{V}$$
4	3	brbigcup	$$⊢A\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\bigcup A\leftrightarrow \bigcup A=\bigcup A$$
5	2 4	mpbir	$$⊢A\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\bigcup A$$
6		fnbigcup	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}Fn\mathrm{V}$$
7		fnbrfvb	$$⊢\left(\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}Fn\mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\left(A\right)=\bigcup A\leftrightarrow A\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\bigcup A\right)$$
8	6 1 7	mp2an	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\left(A\right)=\bigcup A\leftrightarrow A\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\bigcup A$$
9	5 8	mpbir	$$⊢\mathrm{𝖡𝗂𝗀𝖼𝗎𝗉}\left(A\right)=\bigcup A$$