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 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 dom F ∃! x A F x
9 imasng A dom F F A = y | A F y
10 9 adantr A dom F ∃! 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