# Metamath Proof Explorer

## Theorem fsn2g

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by Thierry Arnoux, 11-Jul-2020)

Ref Expression
Assertion fsn2g ${⊢}{A}\in {V}\to \left({F}:\left\{{A}\right\}⟶{B}↔\left({F}\left({A}\right)\in {B}\wedge {F}=\left\{⟨{A},{F}\left({A}\right)⟩\right\}\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\}⟶{B}↔{F}:\left\{{A}\right\}⟶{B}\right)$
3 fveq2 ${⊢}{a}={A}\to {F}\left({a}\right)={F}\left({A}\right)$
4 3 eleq1d ${⊢}{a}={A}\to \left({F}\left({a}\right)\in {B}↔{F}\left({A}\right)\in {B}\right)$
5 id ${⊢}{a}={A}\to {a}={A}$
6 5 3 opeq12d ${⊢}{a}={A}\to ⟨{a},{F}\left({a}\right)⟩=⟨{A},{F}\left({A}\right)⟩$
7 6 sneqd ${⊢}{a}={A}\to \left\{⟨{a},{F}\left({a}\right)⟩\right\}=\left\{⟨{A},{F}\left({A}\right)⟩\right\}$
8 7 eqeq2d ${⊢}{a}={A}\to \left({F}=\left\{⟨{a},{F}\left({a}\right)⟩\right\}↔{F}=\left\{⟨{A},{F}\left({A}\right)⟩\right\}\right)$
9 4 8 anbi12d ${⊢}{a}={A}\to \left(\left({F}\left({a}\right)\in {B}\wedge {F}=\left\{⟨{a},{F}\left({a}\right)⟩\right\}\right)↔\left({F}\left({A}\right)\in {B}\wedge {F}=\left\{⟨{A},{F}\left({A}\right)⟩\right\}\right)\right)$
10 vex ${⊢}{a}\in \mathrm{V}$
11 10 fsn2 ${⊢}{F}:\left\{{a}\right\}⟶{B}↔\left({F}\left({a}\right)\in {B}\wedge {F}=\left\{⟨{a},{F}\left({a}\right)⟩\right\}\right)$
12 2 9 11 vtoclbg ${⊢}{A}\in {V}\to \left({F}:\left\{{A}\right\}⟶{B}↔\left({F}\left({A}\right)\in {B}\wedge {F}=\left\{⟨{A},{F}\left({A}\right)⟩\right\}\right)\right)$