| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: A function maps a singleton to a singleton iff it is the singleton of a ordered pair. |
| Ref | Expression |
|---|---|
| fsn.1 |
|
| fsn.2 |
|
| Ref | Expression |
|---|---|
| fsn |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | visset 2295 |
. . . . . . . . 9
| |
| 2 | 1 | opelf 4579 |
. . . . . . . 8
|
| 3 | elsn 3058 |
. . . . . . . . 9
| |
| 4 | elsn 3058 |
. . . . . . . . 9
| |
| 5 | 3, 4 | anbi12i 540 |
. . . . . . . 8
|
| 6 | 2, 5 | sylib 215 |
. . . . . . 7
|
| 7 | 6 | ex 402 |
. . . . . 6
|
| 8 | opeq12 3160 |
. . . . . . . 8
| |
| 9 | 8 | eleq1d 1963 |
. . . . . . 7
|
| 10 | fsn.1 |
. . . . . . . . . 10
| |
| 11 | 10 | snid 3069 |
. . . . . . . . 9
|
| 12 | feu 4588 |
. . . . . . . . 9
| |
| 13 | 11, 12 | mpan2 760 |
. . . . . . . 8
|
| 14 | fsn.2 |
. . . . . . . . . . 11
| |
| 15 | 14 | eueq1 2428 |
. . . . . . . . . 10
|
| 16 | 15 | biantru 793 |
. . . . . . . . 9
|
| 17 | euanv 1832 |
. . . . . . . . 9
| |
| 18 | opeq2 3159 |
. . . . . . . . . . . . . 14
| |
| 19 | 18 | eleq1d 1963 |
. . . . . . . . . . . . 13
|
| 20 | 19 | pm5.32i 707 |
. . . . . . . . . . . 12
|
| 21 | 4 | anbi1i 539 |
. . . . . . . . . . . 12
|
| 22 | ancom 482 |
. . . . . . . . . . . 12
| |
| 23 | 20, 21, 22 | 3bitr4ri 201 |
. . . . . . . . . . 11
|
| 24 | 23 | eubii 1780 |
. . . . . . . . . 10
|
| 25 | df-reu 2111 |
. . . . . . . . . 10
| |
| 26 | 24, 25 | bitr4i 193 |
. . . . . . . . 9
|
| 27 | 16, 17, 26 | 3bitr2i 196 |
. . . . . . . 8
|
| 28 | 13, 27 | sylibr 217 |
. . . . . . 7
|
| 29 | 9, 28 | syl5cbir 228 |
. . . . . 6
|
| 30 | 7, 29 | impbid 574 |
. . . . 5
|
| 31 | opex 3527 |
. . . . . . 7
| |
| 32 | 31 | elsnc 3065 |
. . . . . 6
|
| 33 | visset 2295 |
. . . . . . 7
| |
| 34 | 33, 1, 14 | opth 3532 |
. . . . . 6
|
| 35 | 32, 34 | bitr2i 191 |
. . . . 5
|
| 36 | 30, 35 | syl6bb 595 |
. . . 4
|
| 37 | 36 | 19.21aivv 1665 |
. . 3
|
| 38 | eqrel 4077 |
. . . 4
| |
| 39 | frel 4566 |
. . . 4
| |
| 40 | 10 | relsn 4087 |
. . . 4
|
| 41 | 38, 39, 40 | sylancl 525 |
. . 3
|
| 42 | 37, 41 | mpbird 213 |
. 2
|
| 43 | 10, 14 | f1osn 4674 |
. . . 4
|
| 44 | f1oeq1 4630 |
. . . 4
| |
| 45 | 43, 44 | mpbiri 211 |
. . 3
|
| 46 | f1of 4635 |
. . 3
| |
| 47 | 45, 46 | syl 12 |
. 2
|
| 48 | 42, 47 | impbii 174 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: xpsn 4808 fsn2 4809 mapsn 5404 bnj134 12478 fdc 15812 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-reu 2111 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-br 3339 df-opab 3396 df-id 3586 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 |