![]() |
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 2621 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2621 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elex 2621 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | jaoi 669 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | eleq1 2145 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | eleq1 2145 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | orbi12d 740 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | df-un 2988 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | elab2g 2750 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 1, 4, 9 | pm5.21nii 653 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-v 2614 df-un 2988 |
This theorem is referenced by: uneqri 3126 uncom 3128 uneq1 3131 unass 3141 ssun1 3147 unss1 3153 ssequn1 3154 unss 3158 rexun 3164 ralunb 3165 unssdif 3217 unssin 3221 inssun 3222 indi 3229 undi 3230 difundi 3234 difindiss 3236 undif3ss 3243 symdifxor 3248 rabun2 3261 reuun2 3265 undif4 3327 ssundifim 3347 dfpr2 3441 eltpg 3462 pwprss 3623 pwtpss 3624 uniun 3646 intun 3693 iunun 3781 iunxun 3782 iinuniss 3784 brun 3857 undifexmid 3991 exmidundif 3998 pwunss 4073 elsuci 4193 elsucg 4194 elsuc2g 4195 ordsucim 4279 sucprcreg 4327 opthprc 4446 xpundi 4451 xpundir 4452 funun 5010 mptun 5096 unpreima 5368 reldmtpos 5949 dftpos4 5959 tpostpos 5960 onunsnss 6553 unfidisj 6558 undifdcss 6559 djulclb 6653 djur 6663 eldju 6665 djuun 6666 eldju2ndl 6669 eldju2ndr 6670 elnn0 8566 un0addcl 8597 un0mulcl 8598 elxnn0 8631 ltxr 9140 elxr 9141 fzsplit2 9358 elfzp1 9378 uzsplit 9398 elfzp12 9405 fz01or 9417 fzosplit 9476 fzouzsplit 9478 elfzonlteqm1 9509 fzosplitsni 9534 hashinfuni 10019 hashennnuni 10021 hashunlem 10046 djulclALT 11043 djurclALT 11044 bj-nntrans 11188 bj-nnelirr 11190 |
Copyright terms: Public domain | W3C validator |