# Metamath Proof Explorer

## Theorem fsng

Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012)

Ref Expression
Assertion fsng ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left({F}:\left\{{A}\right\}⟶\left\{{B}\right\}↔{F}=\left\{⟨{A},{B}⟩\right\}\right)$

### Proof

Step Hyp Ref Expression
1 sneq ${⊢}{a}={A}\to \left\{{a}\right\}=\left\{{A}\right\}$
2 1 feq2d ${⊢}{a}={A}\to \left({F}:\left\{{a}\right\}⟶\left\{{b}\right\}↔{F}:\left\{{A}\right\}⟶\left\{{b}\right\}\right)$
3 opeq1 ${⊢}{a}={A}\to ⟨{a},{b}⟩=⟨{A},{b}⟩$
4 3 sneqd ${⊢}{a}={A}\to \left\{⟨{a},{b}⟩\right\}=\left\{⟨{A},{b}⟩\right\}$
5 4 eqeq2d ${⊢}{a}={A}\to \left({F}=\left\{⟨{a},{b}⟩\right\}↔{F}=\left\{⟨{A},{b}⟩\right\}\right)$
6 2 5 bibi12d ${⊢}{a}={A}\to \left(\left({F}:\left\{{a}\right\}⟶\left\{{b}\right\}↔{F}=\left\{⟨{a},{b}⟩\right\}\right)↔\left({F}:\left\{{A}\right\}⟶\left\{{b}\right\}↔{F}=\left\{⟨{A},{b}⟩\right\}\right)\right)$
7 sneq ${⊢}{b}={B}\to \left\{{b}\right\}=\left\{{B}\right\}$
8 7 feq3d ${⊢}{b}={B}\to \left({F}:\left\{{A}\right\}⟶\left\{{b}\right\}↔{F}:\left\{{A}\right\}⟶\left\{{B}\right\}\right)$
9 opeq2 ${⊢}{b}={B}\to ⟨{A},{b}⟩=⟨{A},{B}⟩$
10 9 sneqd ${⊢}{b}={B}\to \left\{⟨{A},{b}⟩\right\}=\left\{⟨{A},{B}⟩\right\}$
11 10 eqeq2d ${⊢}{b}={B}\to \left({F}=\left\{⟨{A},{b}⟩\right\}↔{F}=\left\{⟨{A},{B}⟩\right\}\right)$
12 8 11 bibi12d ${⊢}{b}={B}\to \left(\left({F}:\left\{{A}\right\}⟶\left\{{b}\right\}↔{F}=\left\{⟨{A},{b}⟩\right\}\right)↔\left({F}:\left\{{A}\right\}⟶\left\{{B}\right\}↔{F}=\left\{⟨{A},{B}⟩\right\}\right)\right)$
13 vex ${⊢}{a}\in \mathrm{V}$
14 vex ${⊢}{b}\in \mathrm{V}$
15 13 14 fsn ${⊢}{F}:\left\{{a}\right\}⟶\left\{{b}\right\}↔{F}=\left\{⟨{a},{b}⟩\right\}$
16 6 12 15 vtocl2g ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left({F}:\left\{{A}\right\}⟶\left\{{B}\right\}↔{F}=\left\{⟨{A},{B}⟩\right\}\right)$