Metamath Proof Explorer

Theorem fnsnfv

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

Ref Expression
Assertion fnsnfv ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left\{{F}\left({B}\right)\right\}={F}\left[\left\{{B}\right\}\right]$

Proof

Step Hyp Ref Expression
1 eqcom ${⊢}{y}={F}\left({B}\right)↔{F}\left({B}\right)={y}$
2 fnbrfvb ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({F}\left({B}\right)={y}↔{B}{F}{y}\right)$
3 1 2 syl5bb ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left({y}={F}\left({B}\right)↔{B}{F}{y}\right)$
4 3 abbidv ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left\{{y}|{y}={F}\left({B}\right)\right\}=\left\{{y}|{B}{F}{y}\right\}$
5 df-sn ${⊢}\left\{{F}\left({B}\right)\right\}=\left\{{y}|{y}={F}\left({B}\right)\right\}$
6 5 a1i ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left\{{F}\left({B}\right)\right\}=\left\{{y}|{y}={F}\left({B}\right)\right\}$
7 fnrel ${⊢}{F}Fn{A}\to \mathrm{Rel}{F}$
8 relimasn ${⊢}\mathrm{Rel}{F}\to {F}\left[\left\{{B}\right\}\right]=\left\{{y}|{B}{F}{y}\right\}$
9 7 8 syl ${⊢}{F}Fn{A}\to {F}\left[\left\{{B}\right\}\right]=\left\{{y}|{B}{F}{y}\right\}$
10 9 adantr ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to {F}\left[\left\{{B}\right\}\right]=\left\{{y}|{B}{F}{y}\right\}$
11 4 6 10 3eqtr4d ${⊢}\left({F}Fn{A}\wedge {B}\in {A}\right)\to \left\{{F}\left({B}\right)\right\}={F}\left[\left\{{B}\right\}\right]$