New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > elun | Unicode version |
Description: Membership in union. (Contributed by SF, 10-Jan-2015.) |
Ref | Expression |
---|---|
elun |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2867 | . 2 | |
2 | elex 2867 | . . 3 | |
3 | elex 2867 | . . 3 | |
4 | 2, 3 | jaoi 368 | . 2 |
5 | elning 3217 | . . . 4 ∼ &ncap ∼ ∼ ∼ | |
6 | elcomplg 3218 | . . . . 5 ∼ | |
7 | elcomplg 3218 | . . . . 5 ∼ | |
8 | 6, 7 | nanbi12d 1303 | . . . 4 ∼ ∼ |
9 | 5, 8 | bitrd 244 | . . 3 ∼ &ncap ∼ |
10 | df-un 3214 | . . . 4 ∼ &ncap ∼ | |
11 | 10 | eleq2i 2417 | . . 3 ∼ &ncap ∼ |
12 | oran 482 | . . . 4 | |
13 | df-nan 1288 | . . . 4 | |
14 | 12, 13 | bitr4i 243 | . . 3 |
15 | 9, 11, 14 | 3bitr4g 279 | . 2 |
16 | 1, 4, 15 | pm5.21nii 342 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wb 176 wo 357 wa 358 wnan 1287 wcel 1710 cvv 2859 &ncap cnin 3204 ∼ ccompl 3205 cun 3207 |
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-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-nin 3211 df-compl 3212 df-un 3214 |
This theorem is referenced by: elsymdif 3223 uneqri 3406 uncom 3408 uneq1 3411 unass 3420 ssun1 3426 unss1 3432 ssequn1 3433 unss 3437 rexun 3443 ralunb 3444 indi 3501 undi 3502 unineq 3505 undif3 3515 symdif2 3520 rabun2 3534 reuun2 3538 undif4 3607 ssundif 3633 dfpr2 3749 eltpg 3769 pwpr 3883 pwtp 3884 unipr 3905 uniun 3910 intun 3958 iinun2 4032 iunun 4046 iunxun 4047 iinuni 4049 pwadjoin 4119 pw1un 4163 dfimak2 4298 dfaddc2 4381 nnsucelrlem1 4424 nnsucelrlem2 4425 nndisjeq 4429 ltfinex 4464 ltfintrilem1 4465 eqtfinrelk 4486 evenfinex 4503 oddfinex 4504 evenoddnnnul 4514 evenodddisjlem1 4515 nnadjoinlem1 4519 vfinspss 4551 vinf 4555 dfphi2 4569 dfop2lem1 4573 phi011lem1 4598 proj1op 4600 proj2op 4601 eqop 4611 brun 4692 setconslem2 4732 setconslem3 4733 setconslem7 4737 dfswap2 4741 xpundi 4832 xpundir 4833 dmun 4912 funun 5146 unpreima 5408 fvclss 5462 cupex 5816 clos1baseima 5883 connexex 5913 enadjlem1 6059 enadj 6060 enprmaplem4 6079 fce 6188 leconnnc 6218 nmembers1lem3 6270 nncdiv3lem2 6276 nchoicelem6 6294 nchoicelem18 6306 |
Copyright terms: Public domain | W3C validator |