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	$$⊢\underset{\_}{Ⅎ}yA$$
	funfv2f.2	$$⊢\underset{\_}{Ⅎ}yF$$
Assertion	funfv2f	$$⊢\mathrm{Fun}F\to F\left(A\right)=\bigcup \left\{y|AFy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funfv2f.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		funfv2f.2	$$⊢\underset{\_}{Ⅎ}yF$$
3		funfv2	$$⊢\mathrm{Fun}F\to F\left(A\right)=\bigcup \left\{w|AFw\right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yw$$
5	1 2 4	nfbr	$$⊢ℲyAFw$$
6		nfv	$$⊢ℲwAFy$$
7		breq2	$$⊢w=y\to \left(AFw\leftrightarrow AFy\right)$$
8	5 6 7	cbvabw	$$⊢\left\{w|AFw\right\}=\left\{y|AFy\right\}$$
9	8	unieqi	$$⊢\bigcup \left\{w|AFw\right\}=\bigcup \left\{y|AFy\right\}$$
10	3 9	eqtrdi	$$⊢\mathrm{Fun}F\to F\left(A\right)=\bigcup \left\{y|AFy\right\}$$