Theorem funiunfvf

Description: The indexed union of a function's values is the union of its image under the index class. This version of funiunfv uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by NM, 26-Mar-2006) (Revised by David Abernethy, 15-Apr-2013)

	Ref	Expression
Hypothesis	funiunfvf.1	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	funiunfvf	$$⊢\mathrm{Fun}F\to \bigcup _{x\in A}F\left(x\right)=\bigcup F\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		funiunfvf.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
3	1 2	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(z\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}zF\left(x\right)$$
5		fveq2	$$⊢z=x\to F\left(z\right)=F\left(x\right)$$
6	3 4 5	cbviun	$$⊢\bigcup _{z\in A}F\left(z\right)=\bigcup _{x\in A}F\left(x\right)$$
7		funiunfv	$$⊢\mathrm{Fun}F\to \bigcup _{z\in A}F\left(z\right)=\bigcup F\left[A\right]$$
8	6 7	eqtr3id	$$⊢\mathrm{Fun}F\to \bigcup _{x\in A}F\left(x\right)=\bigcup F\left[A\right]$$