![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unisn | Structured version Visualization version Unicode version |
Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
unisn.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
unisn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsn2 3993 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | unieqi 4221 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | unisn.1 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3, 3 | unipr 4225 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | unidm 3589 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 2, 4, 5 | 3eqtri 2488 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rex 2755 df-v 3059 df-un 3421 df-sn 3981 df-pr 3983 df-uni 4213 |
This theorem is referenced by: unisng 4228 uniintsn 4286 unidif0 4593 op1sta 5341 op2nda 5344 opswap 5346 unisuc 5522 uniabio 5579 fvssunirn 5915 opabiotafun 5954 funfv 5960 dffv2 5966 onuninsuci 6699 en1b 7668 tc2 8257 cflim2 8724 fin1a2lem10 8870 fin1a2lem12 8872 incexclem 13949 acsmapd 16479 pmtrprfval 17183 sylow2a 17326 lspuni0 18288 lss0v 18294 zrhval2 19135 indistopon 20071 refun0 20585 1stckgenlem 20623 qtopeu 20786 hmphindis 20867 filcon 20953 ufildr 21001 alexsubALTlem3 21119 ptcmplem2 21123 cnextfres1 21138 icccmplem1 21895 disjabrex 28246 disjabrexf 28247 locfinref 28719 pstmfval 28750 esumval 28918 esumpfinval 28947 esumpfinvalf 28948 prsiga 29004 fiunelcarsg 29198 carsgclctunlem1 29199 carsggect 29200 indispcon 30007 fobigcup 30717 onsucsuccmpi 31153 bj-nuliotaALT 31670 mbfresfi 32033 heiborlem3 32191 prsal 38280 isomenndlem 38459 |
Copyright terms: Public domain | W3C validator |