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	|- F/_ y A
	funfv2f.2	|- F/_ y F
Assertion	funfv2f	|- ( Fun F -> ( F ` A ) = U. { y | A F y } )

Proof

Step	Hyp	Ref	Expression
1		funfv2f.1	|- F/_ y A
2		funfv2f.2	|- F/_ y F
3		funfv2	|- ( Fun F -> ( F ` A ) = U. { w | A F w } )
4		nfcv	|- F/_ y w
5	1 2 4	nfbr	|- F/ y A F w
6		nfv	|- F/ w A F y
7		breq2	|- ( w = y -> ( A F w <-> A F y ) )
8	5 6 7	cbvabw	|- { w | A F w } = { y | A F y }
9	8	unieqi	|- U. { w | A F w } = U. { y | A F y }
10	3 9	eqtrdi	|- ( Fun F -> ( F ` A ) = U. { y | A F y } )