Theorem fvbigcup

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

	Ref	Expression
Hypothesis	fvbigcup.1	|- A e. _V
Assertion	fvbigcup	|- ( Bigcup ` A ) = U. A

Proof

Step	Hyp	Ref	Expression
1		fvbigcup.1	|- A e. _V
2		eqid	|- U. A = U. A
3	1	uniex	|- U. A e. _V
4	3	brbigcup	|- ( A Bigcup U. A <-> U. A = U. A )
5	2 4	mpbir	|- A Bigcup U. A
6		fnbigcup	|- Bigcup Fn _V
7		fnbrfvb	|- ( ( Bigcup Fn _V /\ A e. _V ) -> ( ( Bigcup ` A ) = U. A <-> A Bigcup U. A ) )
8	6 1 7	mp2an	|- ( ( Bigcup ` A ) = U. A <-> A Bigcup U. A )
9	5 8	mpbir	|- ( Bigcup ` A ) = U. A