Theorem funressnvmo

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	funressnvmo	⊢ ( Fun ( 𝐹 ↾ { 𝑥 } ) → ∃* 𝑦 𝑥 𝐹 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		dffun6	⊢ ( Fun ( 𝐹 ↾ { 𝑥 } ) ↔ ( Rel ( 𝐹 ↾ { 𝑥 } ) ∧ ∀ 𝑧 ∃* 𝑦 𝑧 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ) )
2		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ↔ 𝑧 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ) )
3	2	equcoms	⊢ ( 𝑧 = 𝑥 → ( 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ↔ 𝑧 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ) )
4	3	biimpd	⊢ ( 𝑧 = 𝑥 → ( 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 → 𝑧 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ) )
5	4	moimdv	⊢ ( 𝑧 = 𝑥 → ( ∃* 𝑦 𝑧 ( 𝐹 ↾ { 𝑥 } ) 𝑦 → ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ) )
6	5	spimvw	⊢ ( ∀ 𝑧 ∃* 𝑦 𝑧 ( 𝐹 ↾ { 𝑥 } ) 𝑦 → ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 )
7		vsnid	⊢ 𝑥 ∈ { 𝑥 }
8		vex	⊢ 𝑦 ∈ V
9	8	brresi	⊢ ( 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝑥 } ∧ 𝑥 𝐹 𝑦 ) )
10	7 9	mpbiran	⊢ ( 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 ↔ 𝑥 𝐹 𝑦 )
11	10	biimpri	⊢ ( 𝑥 𝐹 𝑦 → 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 )
12	11	moimi	⊢ ( ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝑥 } ) 𝑦 → ∃* 𝑦 𝑥 𝐹 𝑦 )
13	6 12	syl	⊢ ( ∀ 𝑧 ∃* 𝑦 𝑧 ( 𝐹 ↾ { 𝑥 } ) 𝑦 → ∃* 𝑦 𝑥 𝐹 𝑦 )
14	1 13	simplbiim	⊢ ( Fun ( 𝐹 ↾ { 𝑥 } ) → ∃* 𝑦 𝑥 𝐹 𝑦 )