Metamath Proof Explorer


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 syl5bb ( 𝐹 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 𝐴 → { ( 𝐹 '''' 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )