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 2566 | . 2 | |
2 | elex 2566 | . . 3 | |
3 | elex 2566 | . . 3 | |
4 | 2, 3 | jaoi 636 | . 2 |
5 | eleq1 2100 | . . . 4 | |
6 | eleq1 2100 | . . . 4 | |
7 | 5, 6 | orbi12d 707 | . . 3 |
8 | df-un 2922 | . . 3 | |
9 | 7, 8 | elab2g 2689 | . 2 |
10 | 1, 4, 9 | pm5.21nii 620 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 98 wo 629 wceq 1243 wcel 1393 cvv 2557 cun 2915 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-v 2559 df-un 2922 |
This theorem is referenced by: uneqri 3085 uncom 3087 uneq1 3090 unass 3100 ssun1 3106 unss1 3112 ssequn1 3113 unss 3117 rexun 3123 ralunb 3124 unssdif 3172 unssin 3176 inssun 3177 indi 3184 undi 3185 difundi 3189 difindiss 3191 undif3ss 3198 symdifxor 3203 rabun2 3216 reuun2 3220 undif4 3284 ssundifim 3306 dfpr2 3394 eltpg 3416 pwprss 3576 pwtpss 3577 uniun 3599 intun 3646 iunun 3734 iunxun 3735 iinuniss 3737 brun 3810 pwunss 4020 elsuci 4140 elsucg 4141 elsuc2g 4142 ordsucim 4226 sucprcreg 4273 opthprc 4391 xpundi 4396 xpundir 4397 funun 4944 mptun 5029 unpreima 5292 reldmtpos 5868 dftpos4 5878 tpostpos 5879 onunsnss 6355 elnn0 8183 un0addcl 8215 un0mulcl 8216 ltxr 8695 elxr 8696 fzsplit2 8914 elfzp1 8934 uzsplit 8954 elfzp12 8961 fzosplit 9033 fzouzsplit 9035 elfzonlteqm1 9066 fzosplitsni 9091 bj-nntrans 10076 bj-nnelirr 10078 |
Copyright terms: Public domain | W3C validator |