Theorem funressneu

Description: There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu . A e. _V is required because otherwise E! y A F y , see brprcneu . (Contributed by AV, 7-Sep-2022)

	Ref	Expression
Assertion	funressneu	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → ∃! 𝑦 𝐴 𝐹 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		simp1l	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → 𝐴 ∈ 𝑉 )
2		simp1r	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → 𝐵 ∈ 𝑊 )
3		simp3	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → 𝐴 𝐹 𝐵 )
4		breldmg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 𝐹 𝐵 ) → 𝐴 ∈ dom 𝐹 )
5	1 2 3 4	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → 𝐴 ∈ dom 𝐹 )
6		eldmg	⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝐴 ∈ dom 𝐹 ↔ ∃ 𝑦 𝐴 𝐹 𝑦 ) )
7	6	ibi	⊢ ( 𝐴 ∈ dom 𝐹 → ∃ 𝑦 𝐴 𝐹 𝑦 )
8	5 7	syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → ∃ 𝑦 𝐴 𝐹 𝑦 )
9		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
10	9	anim1i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐴 ∈ 𝑉 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
11	10	3adant3	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → ( 𝐴 ∈ 𝑉 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
12		funressnmo	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ∃* 𝑦 𝐴 𝐹 𝑦 )
13	11 12	syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → ∃* 𝑦 𝐴 𝐹 𝑦 )
14		moeu	⊢ ( ∃* 𝑦 𝐴 𝐹 𝑦 ↔ ( ∃ 𝑦 𝐴 𝐹 𝑦 → ∃! 𝑦 𝐴 𝐹 𝑦 ) )
15	13 14	sylib	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → ( ∃ 𝑦 𝐴 𝐹 𝑦 → ∃! 𝑦 𝐴 𝐹 𝑦 ) )
16	8 15	mpd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 𝐹 𝐵 ) → ∃! 𝑦 𝐴 𝐹 𝑦 )