Theorem funfv2f

Description: The value of a function. Version of funfv2 using a bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 19-Feb-2006)

	Ref	Expression
Hypotheses	funfv2f.1	⊢ Ⅎ 𝑦 𝐴
	funfv2f.2	⊢ Ⅎ 𝑦 𝐹
Assertion	funfv2f	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑦 ∣ 𝐴 𝐹 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		funfv2f.1	⊢ Ⅎ 𝑦 𝐴
2		funfv2f.2	⊢ Ⅎ 𝑦 𝐹
3		funfv2	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑤 ∣ 𝐴 𝐹 𝑤 } )
4		nfcv	⊢ Ⅎ 𝑦 𝑤
5	1 2 4	nfbr	⊢ Ⅎ 𝑦 𝐴 𝐹 𝑤
6		nfv	⊢ Ⅎ 𝑤 𝐴 𝐹 𝑦
7		breq2	⊢ ( 𝑤 = 𝑦 → ( 𝐴 𝐹 𝑤 ↔ 𝐴 𝐹 𝑦 ) )
8	5 6 7	cbvabw	⊢ { 𝑤 ∣ 𝐴 𝐹 𝑤 } = { 𝑦 ∣ 𝐴 𝐹 𝑦 }
9	8	unieqi	⊢ ∪ { 𝑤 ∣ 𝐴 𝐹 𝑤 } = ∪ { 𝑦 ∣ 𝐴 𝐹 𝑦 }
10	3 9	eqtrdi	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∪ { 𝑦 ∣ 𝐴 𝐹 𝑦 } )