Metamath Proof Explorer


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 ) )