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 | ||
Assertion | funiunfvf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funiunfvf.1 | ||
2 | nfcv | ||
3 | 1 2 | nffv | |
4 | nfcv | ||
5 | fveq2 | ||
6 | 3 4 5 | cbviun | |
7 | funiunfv | ||
8 | 6 7 | eqtr3id |