Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elun | Unicode version |
Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.) |
Ref | Expression |
---|---|
elun |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2671 | . 2 | |
2 | elex 2671 | . . 3 | |
3 | elex 2671 | . . 3 | |
4 | 2, 3 | jaoi 690 | . 2 |
5 | eleq1 2180 | . . . 4 | |
6 | eleq1 2180 | . . . 4 | |
7 | 5, 6 | orbi12d 767 | . . 3 |
8 | df-un 3045 | . . 3 | |
9 | 7, 8 | elab2g 2804 | . 2 |
10 | 1, 4, 9 | pm5.21nii 678 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 682 wceq 1316 wcel 1465 cvv 2660 cun 3039 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 df-un 3045 |
This theorem is referenced by: uneqri 3188 uncom 3190 uneq1 3193 unass 3203 ssun1 3209 unss1 3215 ssequn1 3216 unss 3220 rexun 3226 ralunb 3227 unssdif 3281 unssin 3285 inssun 3286 indi 3293 undi 3294 difundi 3298 difindiss 3300 undif3ss 3307 symdifxor 3312 rabun2 3325 reuun2 3329 undif4 3395 ssundifim 3416 dcun 3443 dfpr2 3516 eltpg 3539 pwprss 3702 pwtpss 3703 uniun 3725 intun 3772 iunun 3861 iunxun 3862 iinuniss 3865 brun 3949 undifexmid 4087 exmidundif 4099 exmidundifim 4100 pwunss 4175 elsuci 4295 elsucg 4296 elsuc2g 4297 ordsucim 4386 sucprcreg 4434 opthprc 4560 xpundi 4565 xpundir 4566 funun 5137 mptun 5224 unpreima 5513 reldmtpos 6118 dftpos4 6128 tpostpos 6129 onunsnss 6773 unfidisj 6778 undifdcss 6779 fidcenumlemrks 6809 djulclb 6908 eldju 6921 eldju2ndl 6925 eldju2ndr 6926 ctssdccl 6964 elnn0 8937 un0addcl 8968 un0mulcl 8969 elxnn0 9000 ltxr 9517 elxr 9518 fzsplit2 9785 elfzp1 9807 uzsplit 9827 elfzp12 9834 fz01or 9846 fzosplit 9909 fzouzsplit 9911 elfzonlteqm1 9942 fzosplitsni 9967 hashinfuni 10478 hashennnuni 10480 hashunlem 10505 zfz1isolemiso 10537 summodclem3 11104 fsumsplit 11131 fsumsplitsn 11134 sumsplitdc 11156 reopnap 12618 djulclALT 12904 djurclALT 12905 bj-nntrans 13045 bj-nnelirr 13047 exmid1stab 13091 |
Copyright terms: Public domain | W3C validator |