Theorem fnressn

Description: A function restricted to a singleton. (Contributed by NM, 9-Oct-2004)

	Ref	Expression
Assertion	fnressn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑥 = 𝐵 → { 𝑥 } = { 𝐵 } )
2	1	reseq2d	⊢ ( 𝑥 = 𝐵 → ( 𝐹 ↾ { 𝑥 } ) = ( 𝐹 ↾ { 𝐵 } ) )
3		fveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
4		opeq12	⊢ ( ( 𝑥 = 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ )
5	3 4	mpdan	⊢ ( 𝑥 = 𝐵 → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ )
6	5	sneqd	⊢ ( 𝑥 = 𝐵 → { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
7	2 6	eqeq12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ↔ ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
8	7	imbi2d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) ↔ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) ) )
9		vex	⊢ 𝑥 ∈ V
10	9	snss	⊢ ( 𝑥 ∈ 𝐴 ↔ { 𝑥 } ⊆ 𝐴 )
11		fnssres	⊢ ( ( 𝐹 Fn 𝐴 ∧ { 𝑥 } ⊆ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } )
12	10 11	sylan2b	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } )
13		dffn2	⊢ ( ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } ↔ ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ V )
14	9	fsn2	⊢ ( ( 𝐹 ↾ { 𝑥 } ) : { 𝑥 } ⟶ V ↔ ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) )
15		fvex	⊢ ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V
16	15	biantrur	⊢ ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ↔ ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) )
17		vsnid	⊢ 𝑥 ∈ { 𝑥 }
18		fvres	⊢ ( 𝑥 ∈ { 𝑥 } → ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19	17 18	ax-mp	⊢ ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
20	19	opeq2i	⊢ ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩
21	20	sneqi	⊢ { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ }
22	21	eqeq2i	⊢ ( ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ↔ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
23	16 22	bitr3i	⊢ ( ( ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ∈ V ∧ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( ( 𝐹 ↾ { 𝑥 } ) ‘ 𝑥 ) ⟩ } ) ↔ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
24	13 14 23	3bitri	⊢ ( ( 𝐹 ↾ { 𝑥 } ) Fn { 𝑥 } ↔ ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
25	12 24	sylib	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
26	25	expcom	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } ) )
27	8 26	vtoclga	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
28	27	impcom	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝐵 } ) = { ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )