fnbrfvb

Description: Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	fnbrfvb	$⊢ (F Fn A \land B \in A) \to (F (B) = C \leftrightarrow B F C)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ F (B) = F (B)$
2		fvex	$⊢ F (B) \in V$
3		eqeq2	$⊢ x = F (B) \to (F (B) = x \leftrightarrow F (B) = F (B))$
4		breq2	$⊢ x = F (B) \to (B F x \leftrightarrow B F F (B))$
5	3 4	bibi12d	$⊢ x = F (B) \to ((F (B) = x \leftrightarrow B F x) \leftrightarrow (F (B) = F (B) \leftrightarrow B F F (B)))$
6	5	imbi2d	$⊢ x = F (B) \to (((F Fn A \land B \in A) \to (F (B) = x \leftrightarrow B F x)) \leftrightarrow ((F Fn A \land B \in A) \to (F (B) = F (B) \leftrightarrow B F F (B))))$
7		fneu	$⊢ (F Fn A \land B \in A) \to \exists! x B F x$
8		tz6.12c	$⊢ \exists! x B F x \to (F (B) = x \leftrightarrow B F x)$
9	7 8	syl	$⊢ (F Fn A \land B \in A) \to (F (B) = x \leftrightarrow B F x)$
10	2 6 9	vtocl	$⊢ (F Fn A \land B \in A) \to (F (B) = F (B) \leftrightarrow B F F (B))$
11	1 10	mpbii	$⊢ (F Fn A \land B \in A) \to B F F (B)$
12		breq2	$⊢ F (B) = C \to (B F F (B) \leftrightarrow B F C)$
13	11 12	syl5ibcom	$⊢ (F Fn A \land B \in A) \to (F (B) = C \to B F C)$
14		fnfun	$⊢ F Fn A \to Fun F$
15		funbrfv	$⊢ Fun F \to (B F C \to F (B) = C)$
16	14 15	syl	$⊢ F Fn A \to (B F C \to F (B) = C)$
17	16	adantr	$⊢ (F Fn A \land B \in A) \to (B F C \to F (B) = C)$
18	13 17	impbid	$⊢ (F Fn A \land B \in A) \to (F (B) = C \leftrightarrow B F C)$

Metamath Proof Explorer