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	|- F/_ x F
Assertion	funiunfvf	|- ( Fun F -> U_ x e. A ( F ` x ) = U. ( F " A ) )

Proof

Step	Hyp	Ref	Expression
1		funiunfvf.1	|- F/_ x F
2		nfcv	|- F/_ x z
3	1 2	nffv	|- F/_ x ( F ` z )
4		nfcv	|- F/_ z ( F ` x )
5		fveq2	|- ( z = x -> ( F ` z ) = ( F ` x ) )
6	3 4 5	cbviun	|- U_ z e. A ( F ` z ) = U_ x e. A ( F ` x )
7		funiunfv	|- ( Fun F -> U_ z e. A ( F ` z ) = U. ( F " A ) )
8	6 7	eqtr3id	|- ( Fun F -> U_ x e. A ( F ` x ) = U. ( F " A ) )