dfatbrafv2b

Description: Equivalence of function value and binary relation, analogous to fnbrfvb or funbrfvb . B e. _V is required, because otherwise A F B <-> (/) e. F can be true, but ( F '''' A ) = B is always false (because of dfatafv2ex ). (Contributed by AV, 6-Sep-2022)

		Ref	Expression
	Assertion	dfatbrafv2b	$⊢ (F defAt A \land B \in W) \to ((F'''' A) = B \leftrightarrow A F B)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (F'''' A) = (F'''' A)$
2		dfatafv2ex	$⊢ F defAt A \to (F'''' A) \in V$
3	2	adantr	$⊢ (F defAt A \land B \in W) \to (F'''' A) \in V$
4		eqeq2	$⊢ x = (F'''' A) \to ((F'''' A) = x \leftrightarrow (F'''' A) = (F'''' A))$
5		breq2	$⊢ x = (F'''' A) \to (A F x \leftrightarrow A F (F'''' A))$
6	4 5	bibi12d	$⊢ x = (F'''' A) \to (((F'''' A) = x \leftrightarrow A F x) \leftrightarrow ((F'''' A) = (F'''' A) \leftrightarrow A F (F'''' A)))$
7	6	adantl	$⊢ ((F defAt A \land B \in W) \land x = (F'''' A)) \to (((F'''' A) = x \leftrightarrow A F x) \leftrightarrow ((F'''' A) = (F'''' A) \leftrightarrow A F (F'''' A)))$
8		dfdfat2	$⊢ F defAt A \leftrightarrow (A \in dom F \land \exists! x A F x)$
9		tz6.12c-afv2	$⊢ \exists! x A F x \to ((F'''' A) = x \leftrightarrow A F x)$
10	8 9	simplbiim	$⊢ F defAt A \to ((F'''' A) = x \leftrightarrow A F x)$
11	10	adantr	$⊢ (F defAt A \land B \in W) \to ((F'''' A) = x \leftrightarrow A F x)$
12	3 7 11	vtocld	$⊢ (F defAt A \land B \in W) \to ((F'''' A) = (F'''' A) \leftrightarrow A F (F'''' A))$
13	1 12	mpbii	$⊢ (F defAt A \land B \in W) \to A F (F'''' A)$
14		breq2	$⊢ (F'''' A) = B \to (A F (F'''' A) \leftrightarrow A F B)$
15	13 14	syl5ibcom	$⊢ (F defAt A \land B \in W) \to ((F'''' A) = B \to A F B)$
16		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
17		simpll	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land B \in W) \to A \in dom F$
18		simpr	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land B \in W) \to B \in W$
19		simpr	$⊢ (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to Fun ({F ↾}_{\{A\}})$
20	19	adantr	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land B \in W) \to Fun ({F ↾}_{\{A\}})$
21	17 18 20	jca31	$⊢ ((A \in dom F \land Fun ({F ↾}_{\{A\}})) \land B \in W) \to ((A \in dom F \land B \in W) \land Fun ({F ↾}_{\{A\}}))$
22	16 21	sylanb	$⊢ (F defAt A \land B \in W) \to ((A \in dom F \land B \in W) \land Fun ({F ↾}_{\{A\}}))$
23		funressnbrafv2	$⊢ ((A \in dom F \land B \in W) \land Fun ({F ↾}_{\{A\}})) \to (A F B \to (F'''' A) = B)$
24	22 23	syl	$⊢ (F defAt A \land B \in W) \to (A F B \to (F'''' A) = B)$
25	15 24	impbid	$⊢ (F defAt A \land B \in W) \to ((F'''' A) = B \leftrightarrow A F B)$

Metamath Proof Explorer

Theorem dfatbrafv2b

Proof