This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \underline{Ⅎ} x F$
	Assertion	funiunfvf	$⊢ Fun F \to ⋃_{x \in A} F (x) = ⋃ F [A]$

Proof

Step	Hyp	Ref	Expression
1		funiunfvf.1	$⊢ \underline{Ⅎ} x F$
2		nfcv	$⊢ \underline{Ⅎ} x z$
3	1 2	nffv	$⊢ \underline{Ⅎ} x F (z)$
4		nfcv	$⊢ \underline{Ⅎ} z F (x)$
5		fveq2	$⊢ z = x \to F (z) = F (x)$
6	3 4 5	cbviun	$⊢ ⋃_{z \in A} F (z) = ⋃_{x \in A} F (x)$
7		funiunfv	$⊢ Fun F \to ⋃_{z \in A} F (z) = ⋃ F [A]$
8	6 7	eqtr3id	$⊢ Fun F \to ⋃_{x \in A} F (x) = ⋃ F [A]$