# Metamath Proof Explorer

## Theorem funop1

Description: A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020)

Ref Expression
Assertion funop1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=⟨{x},{y}⟩\to \left(\mathrm{Fun}{F}↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}\right)$

### Proof

Step Hyp Ref Expression
1 opeq12 ${⊢}\left({x}={v}\wedge {y}={w}\right)\to ⟨{x},{y}⟩=⟨{v},{w}⟩$
2 1 eqeq2d ${⊢}\left({x}={v}\wedge {y}={w}\right)\to \left({F}=⟨{x},{y}⟩↔{F}=⟨{v},{w}⟩\right)$
3 2 cbvex2vw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=⟨{x},{y}⟩↔\exists {v}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{F}=⟨{v},{w}⟩$
4 vex ${⊢}{v}\in \mathrm{V}$
5 vex ${⊢}{w}\in \mathrm{V}$
6 4 5 funopsn ${⊢}\left(\mathrm{Fun}{F}\wedge {F}=⟨{v},{w}⟩\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{a}\right\}\wedge {F}=\left\{⟨{a},{a}⟩\right\}\right)$
7 vex ${⊢}{a}\in \mathrm{V}$
8 opeq12 ${⊢}\left({x}={a}\wedge {y}={a}\right)\to ⟨{x},{y}⟩=⟨{a},{a}⟩$
9 8 sneqd ${⊢}\left({x}={a}\wedge {y}={a}\right)\to \left\{⟨{x},{y}⟩\right\}=\left\{⟨{a},{a}⟩\right\}$
10 9 eqeq2d ${⊢}\left({x}={a}\wedge {y}={a}\right)\to \left({F}=\left\{⟨{x},{y}⟩\right\}↔{F}=\left\{⟨{a},{a}⟩\right\}\right)$
11 7 7 10 spc2ev ${⊢}{F}=\left\{⟨{a},{a}⟩\right\}\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}$
12 11 adantl ${⊢}\left({v}=\left\{{a}\right\}\wedge {F}=\left\{⟨{a},{a}⟩\right\}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}$
13 12 exlimiv ${⊢}\exists {a}\phantom{\rule{.4em}{0ex}}\left({v}=\left\{{a}\right\}\wedge {F}=\left\{⟨{a},{a}⟩\right\}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}$
14 6 13 syl ${⊢}\left(\mathrm{Fun}{F}\wedge {F}=⟨{v},{w}⟩\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}$
15 14 expcom ${⊢}{F}=⟨{v},{w}⟩\to \left(\mathrm{Fun}{F}\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}\right)$
16 vex ${⊢}{x}\in \mathrm{V}$
17 vex ${⊢}{y}\in \mathrm{V}$
18 16 17 funsn ${⊢}\mathrm{Fun}\left\{⟨{x},{y}⟩\right\}$
19 funeq ${⊢}{F}=\left\{⟨{x},{y}⟩\right\}\to \left(\mathrm{Fun}{F}↔\mathrm{Fun}\left\{⟨{x},{y}⟩\right\}\right)$
20 18 19 mpbiri ${⊢}{F}=\left\{⟨{x},{y}⟩\right\}\to \mathrm{Fun}{F}$
21 20 exlimivv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}\to \mathrm{Fun}{F}$
22 15 21 impbid1 ${⊢}{F}=⟨{v},{w}⟩\to \left(\mathrm{Fun}{F}↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}\right)$
23 22 exlimivv ${⊢}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{F}=⟨{v},{w}⟩\to \left(\mathrm{Fun}{F}↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}\right)$
24 3 23 sylbi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=⟨{x},{y}⟩\to \left(\mathrm{Fun}{F}↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{F}=\left\{⟨{x},{y}⟩\right\}\right)$