fnbrafvb

Description: Equivalence of function value and binary relation, analogous to fnbrfvb . (Contributed by Alexander van der Vekens, 25-May-2017)

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

Step	Hyp	Ref	Expression
1		fndm	$⊢ F Fn A \to dom F = A$
2		eleq2	$⊢ A = dom F \to (B \in A \leftrightarrow B \in dom F)$
3	2	eqcoms	$⊢ dom F = A \to (B \in A \leftrightarrow B \in dom F)$
4	3	biimpd	$⊢ dom F = A \to (B \in A \to B \in dom F)$
5	1 4	syl	$⊢ F Fn A \to (B \in A \to B \in dom F)$
6	5	imp	$⊢ (F Fn A \land B \in A) \to B \in dom F$
7		snssi	$⊢ B \in A \to \{B\} \subseteq A$
8	7	adantl	$⊢ (F Fn A \land B \in A) \to \{B\} \subseteq A$
9		fnssresb	$⊢ F Fn A \to (({F ↾}_{\{B\}}) Fn \{B\} \leftrightarrow \{B\} \subseteq A)$
10	9	adantr	$⊢ (F Fn A \land B \in A) \to (({F ↾}_{\{B\}}) Fn \{B\} \leftrightarrow \{B\} \subseteq A)$
11	8 10	mpbird	$⊢ (F Fn A \land B \in A) \to ({F ↾}_{\{B\}}) Fn \{B\}$
12		fnfun	$⊢ ({F ↾}_{\{B\}}) Fn \{B\} \to Fun ({F ↾}_{\{B\}})$
13	11 12	syl	$⊢ (F Fn A \land B \in A) \to Fun ({F ↾}_{\{B\}})$
14		df-dfat	$⊢ F defAt B \leftrightarrow (B \in dom F \land Fun ({F ↾}_{\{B\}}))$
15		afvfundmfveq	$⊢ F defAt B \to (F''' B) = F (B)$
16	14 15	sylbir	$⊢ (B \in dom F \land Fun ({F ↾}_{\{B\}})) \to (F''' B) = F (B)$
17	6 13 16	syl2anc	$⊢ (F Fn A \land B \in A) \to (F''' B) = F (B)$
18	17	eqeq1d	$⊢ (F Fn A \land B \in A) \to ((F''' B) = C \leftrightarrow F (B) = C)$
19		fnbrfvb	$⊢ (F Fn A \land B \in A) \to (F (B) = C \leftrightarrow B F C)$
20	18 19	bitrd	$⊢ (F Fn A \land B \in A) \to ((F''' B) = C \leftrightarrow B F C)$

Metamath Proof Explorer