Metamath Proof Explorer


Theorem dfatsnafv2

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

Ref Expression
Assertion dfatsnafv2
|- ( F defAt A -> { ( F '''' A ) } = ( F " { A } ) )

Proof

Step Hyp Ref Expression
1 eqcom
 |-  ( y = ( F '''' A ) <-> ( F '''' A ) = y )
2 dfatbrafv2b
 |-  ( ( F defAt A /\ y e. _V ) -> ( ( F '''' A ) = y <-> A F y ) )
3 2 elvd
 |-  ( F defAt A -> ( ( F '''' A ) = y <-> A F y ) )
4 1 3 syl5bb
 |-  ( F defAt A -> ( y = ( F '''' A ) <-> A F y ) )
5 4 abbidv
 |-  ( F defAt A -> { y | y = ( F '''' A ) } = { y | A F y } )
6 df-sn
 |-  { ( F '''' A ) } = { y | y = ( F '''' A ) }
7 6 a1i
 |-  ( F defAt A -> { ( F '''' A ) } = { y | y = ( F '''' A ) } )
8 dfdfat2
 |-  ( F defAt A <-> ( A e. dom F /\ E! x A F x ) )
9 imasng
 |-  ( A e. dom F -> ( F " { A } ) = { y | A F y } )
10 9 adantr
 |-  ( ( A e. dom F /\ E! x A F x ) -> ( F " { A } ) = { y | A F y } )
11 8 10 sylbi
 |-  ( F defAt A -> ( F " { A } ) = { y | A F y } )
12 5 7 11 3eqtr4d
 |-  ( F defAt A -> { ( F '''' A ) } = ( F " { A } ) )