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 _ x F
Assertion funiunfvf Fun F x A F x = F A

Proof

Step Hyp Ref Expression
1 funiunfvf.1 _ x F
2 nfcv _ x z
3 1 2 nffv _ x F z
4 nfcv _ z F x
5 fveq2 z = x F z = F x
6 3 4 5 cbviun z A F z = x A F x
7 funiunfv Fun F z A F z = F A
8 6 7 eqtr3id Fun F x A F x = F A