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