New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > uniintsn | Unicode version |
Description: Two ways to express " is a singleton." See also en1 in set.mm, en1b in set.mm, card1 in set.mm, and eusn 3796. (Contributed by NM, 2-Aug-2010.) |
Ref | Expression |
---|---|
uniintsn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vn0 3557 | . . . . . 6 | |
2 | inteq 3929 | . . . . . . . . . . 11 | |
3 | int0 3940 | . . . . . . . . . . 11 | |
4 | 2, 3 | syl6eq 2401 | . . . . . . . . . 10 |
5 | 4 | adantl 452 | . . . . . . . . 9 |
6 | unieq 3900 | . . . . . . . . . . . 12 | |
7 | uni0 3918 | . . . . . . . . . . . 12 | |
8 | 6, 7 | syl6eq 2401 | . . . . . . . . . . 11 |
9 | eqeq1 2359 | . . . . . . . . . . 11 | |
10 | 8, 9 | syl5ib 210 | . . . . . . . . . 10 |
11 | 10 | imp 418 | . . . . . . . . 9 |
12 | 5, 11 | eqtr3d 2387 | . . . . . . . 8 |
13 | 12 | ex 423 | . . . . . . 7 |
14 | 13 | necon3d 2554 | . . . . . 6 |
15 | 1, 14 | mpi 16 | . . . . 5 |
16 | n0 3559 | . . . . 5 | |
17 | 15, 16 | sylib 188 | . . . 4 |
18 | vex 2862 | . . . . . . 7 | |
19 | vex 2862 | . . . . . . 7 | |
20 | 18, 19 | prss 3861 | . . . . . 6 |
21 | uniss 3912 | . . . . . . . . . . . . 13 | |
22 | 21 | adantl 452 | . . . . . . . . . . . 12 |
23 | simpl 443 | . . . . . . . . . . . 12 | |
24 | 22, 23 | sseqtrd 3307 | . . . . . . . . . . 11 |
25 | intss 3947 | . . . . . . . . . . . 12 | |
26 | 25 | adantl 452 | . . . . . . . . . . 11 |
27 | 24, 26 | sstrd 3282 | . . . . . . . . . 10 |
28 | 18, 19 | unipr 3905 | . . . . . . . . . 10 |
29 | 18, 19 | intpr 3959 | . . . . . . . . . 10 |
30 | 27, 28, 29 | 3sstr3g 3311 | . . . . . . . . 9 |
31 | inss1 3475 | . . . . . . . . . 10 | |
32 | ssun1 3426 | . . . . . . . . . 10 | |
33 | 31, 32 | sstri 3281 | . . . . . . . . 9 |
34 | 30, 33 | jctir 524 | . . . . . . . 8 |
35 | eqss 3287 | . . . . . . . . 9 | |
36 | uneqin 3506 | . . . . . . . . 9 | |
37 | 35, 36 | bitr3i 242 | . . . . . . . 8 |
38 | 34, 37 | sylib 188 | . . . . . . 7 |
39 | 38 | ex 423 | . . . . . 6 |
40 | 20, 39 | syl5bi 208 | . . . . 5 |
41 | 40 | alrimivv 1632 | . . . 4 |
42 | 17, 41 | jca 518 | . . 3 |
43 | euabsn 3792 | . . . 4 | |
44 | eleq1 2413 | . . . . 5 | |
45 | 44 | eu4 2243 | . . . 4 |
46 | abid2 2470 | . . . . . 6 | |
47 | 46 | eqeq1i 2360 | . . . . 5 |
48 | 47 | exbii 1582 | . . . 4 |
49 | 43, 45, 48 | 3bitr3i 266 | . . 3 |
50 | 42, 49 | sylib 188 | . 2 |
51 | 18 | unisn 3907 | . . . 4 |
52 | unieq 3900 | . . . 4 | |
53 | inteq 3929 | . . . . 5 | |
54 | 18 | intsn 3962 | . . . . 5 |
55 | 53, 54 | syl6eq 2401 | . . . 4 |
56 | 51, 52, 55 | 3eqtr4a 2411 | . . 3 |
57 | 56 | exlimiv 1634 | . 2 |
58 | 50, 57 | impbii 180 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wa 358 wal 1540 wex 1541 wceq 1642 wcel 1710 weu 2204 cab 2339 wne 2516 cvv 2859 cun 3207 cin 3208 wss 3257 c0 3550 csn 3737 cpr 3738 cuni 3891 cint 3926 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-ss 3259 df-nul 3551 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 |
This theorem is referenced by: uniintab 3964 |
Copyright terms: Public domain | W3C validator |