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

Metamath Proof Explorer

Theorem fnimasnd

Description: The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023)

Ref Expression
Hypotheses fnimasnd.1 ⊢ φ → F Fn A
fnimasnd.2 ⊢ φ → S ∈ A
Assertion fnimasnd ⊢ φ → F S = F ⁡ S

Proof

Step Hyp Ref Expression
1 fnimasnd.1 ⊢ φ → F Fn A
2 fnimasnd.2 ⊢ φ → S ∈ A
3 fnsnfv ⊢ F Fn A ∧ S ∈ A → F ⁡ S = F S
4 1 2 3 syl2anc ⊢ φ → F ⁡ S = F S
5 4 eqcomd ⊢ φ → F S = F ⁡ S