This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnsnfv

Description: Singleton of function value. (Contributed by NM, 22-May-1998) (Proof shortened by Scott Fenton, 8-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 imasng ⊢ B ∈ A → F B = y | B F y
2 1 adantl ⊢ F Fn A ∧ B ∈ A → F B = y | B F y
3 velsn ⊢ y ∈ F ⁡ B ↔ y = F ⁡ B
4 eqcom ⊢ y = F ⁡ B ↔ F ⁡ B = y
5 3 4 bitri ⊢ y ∈ F ⁡ B ↔ F ⁡ B = y
6 fnbrfvb ⊢ F Fn A ∧ B ∈ A → F ⁡ B = y ↔ B F y
7 5 6 bitr2id ⊢ F Fn A ∧ B ∈ A → B F y ↔ y ∈ F ⁡ B
8 7 eqabcdv ⊢ F Fn A ∧ B ∈ A → y | B F y = F ⁡ B
9 2 8 eqtr2d ⊢ F Fn A ∧ B ∈ A → F ⁡ B = F B