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	bitrid	|- ( 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 } ) )