Theorem funressnbrafv2

Description: The second argument of a binary relation on a function is the function's value, analogous to funbrfv . (Contributed by AV, 7-Sep-2022)

	Ref	Expression
Assertion	funressnbrafv2	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 𝐹 𝐵 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpllr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) → 𝐵 ∈ 𝑊 )
2		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝑊 ↔ 𝐵 ∈ 𝑊 ) )
3	2	anbi2d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) )
4	3	anbi1d	⊢ ( 𝑥 = 𝐵 → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) )
5		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 𝐹 𝑥 ↔ 𝐴 𝐹 𝐵 ) )
6	4 5	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝑥 ) ↔ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) ) )
7		eqeq2	⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 '''' 𝐴 ) = 𝑥 ↔ ( 𝐹 '''' 𝐴 ) = 𝐵 ) )
8	6 7	imbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = 𝑥 ) ↔ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 ) ) )
9		id	⊢ ( 𝐴 𝐹 𝑥 → 𝐴 𝐹 𝑥 )
10		funressneu	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝑥 ) → ∃! 𝑥 𝐴 𝐹 𝑥 )
11	10	3expa	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝑥 ) → ∃! 𝑥 𝐴 𝐹 𝑥 )
12		tz6.12-1-afv2	⊢ ( ( 𝐴 𝐹 𝑥 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = 𝑥 )
13	9 11 12	syl2an2	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝑥 ) → ( 𝐹 '''' 𝐴 ) = 𝑥 )
14	8 13	vtoclg	⊢ ( 𝐵 ∈ 𝑊 → ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )
15	1 14	mpcom	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 '''' 𝐴 ) = 𝐵 )
16	15	ex	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 𝐹 𝐵 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )