![]() |
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 2763 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elex 2763 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elex 2763 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | jaoi 717 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | eleq1 2252 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | eleq1 2252 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | orbi12d 794 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | df-un 3148 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | elab2g 2899 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 1, 4, 9 | pm5.21nii 705 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-un 3148 |
This theorem is referenced by: uneqri 3292 uncom 3294 uneq1 3297 unass 3307 ssun1 3313 unss1 3319 ssequn1 3320 unss 3324 rexun 3330 ralunb 3331 unssdif 3385 unssin 3389 inssun 3390 indi 3397 undi 3398 difundi 3402 difindiss 3404 undif3ss 3411 symdifxor 3416 rabun2 3429 reuun2 3433 undif4 3500 ssundifim 3521 dcun 3548 dfpr2 3626 eltpg 3652 pwprss 3820 pwtpss 3821 uniun 3843 intun 3890 iunun 3980 iunxun 3981 iinuniss 3984 brun 4069 undifexmid 4211 exmidundif 4224 exmidundifim 4225 exmid1stab 4226 pwunss 4301 elsuci 4421 elsucg 4422 elsuc2g 4423 ordsucim 4517 sucprcreg 4566 opthprc 4695 xpundi 4700 xpundir 4701 funun 5279 mptun 5366 unpreima 5662 reldmtpos 6279 dftpos4 6289 tpostpos 6290 onunsnss 6946 unfidisj 6951 undifdcss 6952 fidcenumlemrks 6983 djulclb 7085 eldju 7098 eldju2ndl 7102 eldju2ndr 7103 ctssdccl 7141 pw1nel3 7261 sucpw1nel3 7263 elnn0 9209 un0addcl 9240 un0mulcl 9241 elxnn0 9272 ltxr 9807 elxr 9808 fzsplit2 10082 elfzp1 10104 uzsplit 10124 elfzp12 10131 fz01or 10143 fzosplit 10209 fzouzsplit 10211 elfzonlteqm1 10242 fzosplitsni 10267 hashinfuni 10792 hashennnuni 10794 hashunlem 10819 zfz1isolemiso 10854 summodclem3 11423 fsumsplit 11450 fsumsplitsn 11453 sumsplitdc 11475 fprodsplitdc 11639 fprodsplit 11640 fprodunsn 11647 fprodsplitsn 11676 nnnn0modprm0 12290 prm23lt5 12298 reopnap 14515 lgsdir2 14912 2lgsoddprmlem3 14937 djulclALT 15031 djurclALT 15032 bj-charfun 15037 bj-nntrans 15181 bj-nnelirr 15183 |
Copyright terms: Public domain | W3C validator |