Metamath Proof Explorer

Theorem fnsnfv

Description: Singleton of function value. (Contributed by NM, 22-May-1998)

Ref Expression
Assertion fnsnfv ⊢ F Fn A ∧ B ∈ A → F ⁡ B = F B

Proof

Step Hyp Ref Expression
1 eqcom ⊢ y = F ⁡ B ↔ F ⁡ B = y
2 fnbrfvb ⊢ F Fn A ∧ B ∈ A → F ⁡ B = y ↔ B F y
3 1 2 syl5bb ⊢ F Fn A ∧ B ∈ A → y = F ⁡ B ↔ B F y
4 3 abbidv ⊢ F Fn A ∧ B ∈ A → y | y = F ⁡ B = y | B F y
5 df-sn ⊢ F ⁡ B = y | y = F ⁡ B
6 5 a1i ⊢ F Fn A ∧ B ∈ A → F ⁡ B = y | y = F ⁡ B
7 fnrel ⊢ F Fn A → Rel ⁡ F
8 relimasn ⊢ Rel ⁡ F → F B = y | B F y
9 7 8 syl ⊢ F Fn A → F B = y | B F y
10 9 adantr ⊢ F Fn A ∧ B ∈ A → F B = y | B F y
11 4 6 10 3eqtr4d ⊢ F Fn A ∧ B ∈ A → F ⁡ B = F B