This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \underline{Ⅎ} y A$
	funfv2f.2	$⊢ \underline{Ⅎ} y F$
Assertion	funfv2f	$⊢ Fun F \to F (A) = ⋃ \{y \| A F y\}$

Proof

Step	Hyp	Ref	Expression
1		funfv2f.1	$⊢ \underline{Ⅎ} y A$
2		funfv2f.2	$⊢ \underline{Ⅎ} y F$
3		funfv2	$⊢ Fun F \to F (A) = ⋃ \{w \| A F w\}$
4		nfcv	$⊢ \underline{Ⅎ} y w$
5	1 2 4	nfbr	$⊢ Ⅎ y A F w$
6		nfv	$⊢ Ⅎ w A F y$
7		breq2	$⊢ w = y \to (A F w \leftrightarrow A F y)$
8	5 6 7	cbvabw	$⊢ \{w \| A F w\} = \{y \| A F y\}$
9	8	unieqi	$⊢ ⋃ \{w \| A F w\} = ⋃ \{y \| A F y\}$
10	3 9	eqtrdi	$⊢ Fun F \to F (A) = ⋃ \{y \| A F y\}$