| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > elssuni | Unicode version | ||
| Description: An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.) |
| Ref | Expression |
|---|---|
| elssuni |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssid 3213 |
. 2
| |
| 2 | ssuni 3872 |
. 2
| |
| 3 | 1, 2 | mpan 424 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-v 2774 df-in 3172 df-ss 3179 df-uni 3851 |
| This theorem is referenced by: unissel 3879 ssunieq 3883 pwuni 4236 pwel 4262 uniopel 4301 iunpw 4527 dmrnssfld 4941 iotaexab 5250 fvssunirng 5591 relfvssunirn 5592 sefvex 5597 riotaexg 5903 pwuninel2 6368 tfrlem9 6405 tfrexlem 6420 sbthlem1 7059 sbthlem2 7060 unirnioo 10095 eltopss 14481 toponss 14498 isbasis3g 14518 baspartn 14522 bastg 14533 tgcl 14536 epttop 14562 difopn 14580 ssntr 14594 isopn3 14597 isopn3i 14607 neiuni 14633 resttopon 14643 restopn2 14655 ssidcn 14682 lmtopcnp 14722 txuni2 14728 hmeoimaf1o 14786 tgioo 15026 bj-elssuniab 15727 |
| Copyright terms: Public domain | W3C validator |