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	⊢ Ⅎ 𝑥 𝐹
	Assertion	funiunfvf	⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		funiunfvf.1	⊢ Ⅎ 𝑥 𝐹
2		nfcv	⊢ Ⅎ 𝑥 𝑧
3	1 2	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
4		nfcv	⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑥 )
5		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
6	3 4 5	cbviun	⊢ ∪ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 )
7		funiunfv	⊢ ( Fun 𝐹 → ∪ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ∪ ( 𝐹 “ 𝐴 ) )
8	6 7	eqtr3id	⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ 𝐴 ) )

Metamath Proof Explorer

Theorem funiunfvf

Proof