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 𝑥 𝐹
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 𝐹 𝑥𝐴 ( 𝐹𝑥 ) = ( 𝐹𝐴 ) )