Theorem dfatsnafv2

Description: Singleton of function value, analogous to fnsnfv . (Contributed by AV, 7-Sep-2022)

	Ref	Expression
Assertion	dfatsnafv2	⊢ ( 𝐹 defAt 𝐴 → { ( 𝐹 '''' 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( 𝑦 = ( 𝐹 '''' 𝐴 ) ↔ ( 𝐹 '''' 𝐴 ) = 𝑦 )
2		dfatbrafv2b	⊢ ( ( 𝐹 defAt 𝐴 ∧ 𝑦 ∈ V ) → ( ( 𝐹 '''' 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
3	2	elvd	⊢ ( 𝐹 defAt 𝐴 → ( ( 𝐹 '''' 𝐴 ) = 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
4	1 3	bitrid	⊢ ( 𝐹 defAt 𝐴 → ( 𝑦 = ( 𝐹 '''' 𝐴 ) ↔ 𝐴 𝐹 𝑦 ) )
5	4	abbidv	⊢ ( 𝐹 defAt 𝐴 → { 𝑦 ∣ 𝑦 = ( 𝐹 '''' 𝐴 ) } = { 𝑦 ∣ 𝐴 𝐹 𝑦 } )
6		df-sn	⊢ { ( 𝐹 '''' 𝐴 ) } = { 𝑦 ∣ 𝑦 = ( 𝐹 '''' 𝐴 ) }
7	6	a1i	⊢ ( 𝐹 defAt 𝐴 → { ( 𝐹 '''' 𝐴 ) } = { 𝑦 ∣ 𝑦 = ( 𝐹 '''' 𝐴 ) } )
8		dfdfat2	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
9		imasng	⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝐹 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝐹 𝑦 } )
10	9	adantr	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ ∃! 𝑥 𝐴 𝐹 𝑥 ) → ( 𝐹 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝐹 𝑦 } )
11	8 10	sylbi	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 “ { 𝐴 } ) = { 𝑦 ∣ 𝐴 𝐹 𝑦 } )
12	5 7 11	3eqtr4d	⊢ ( 𝐹 defAt 𝐴 → { ( 𝐹 '''' 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )