Metamath Proof Explorer


Theorem funressnmo

Description: A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion funressnmo ( ( 𝐴𝑉 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ∃* 𝑦 𝐴 𝐹 𝑦 )

Proof

Step Hyp Ref Expression
1 sneq ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
2 1 reseq2d ( 𝑥 = 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = ( 𝐹 ↾ { 𝐴 } ) )
3 2 funeqd ( 𝑥 = 𝐴 → ( Fun ( 𝐹 ↾ { 𝑥 } ) ↔ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
4 breq1 ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦𝐴 𝐹 𝑦 ) )
5 4 mobidv ( 𝑥 = 𝐴 → ( ∃* 𝑦 𝑥 𝐹 𝑦 ↔ ∃* 𝑦 𝐴 𝐹 𝑦 ) )
6 3 5 imbi12d ( 𝑥 = 𝐴 → ( ( Fun ( 𝐹 ↾ { 𝑥 } ) → ∃* 𝑦 𝑥 𝐹 𝑦 ) ↔ ( Fun ( 𝐹 ↾ { 𝐴 } ) → ∃* 𝑦 𝐴 𝐹 𝑦 ) ) )
7 funressnvmo ( Fun ( 𝐹 ↾ { 𝑥 } ) → ∃* 𝑦 𝑥 𝐹 𝑦 )
8 6 7 vtoclg ( 𝐴𝑉 → ( Fun ( 𝐹 ↾ { 𝐴 } ) → ∃* 𝑦 𝐴 𝐹 𝑦 ) )
9 8 imp ( ( 𝐴𝑉 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ∃* 𝑦 𝐴 𝐹 𝑦 )