Metamath Proof Explorer


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 ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 𝐹 𝐵 → ( 𝐹 '''' 𝐴 ) = 𝐵 ) )