Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Alternative definitions of function values (2)
dfatsnafv2
Next ⟩
dfafv23
Metamath Proof Explorer
Ascii
Unicode
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