![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > incom | Unicode version |
Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
incom |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancom 266 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | elin 3333 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | elin 3333 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3bitr4i 212 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | eqriv 2186 |
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-in 3150 |
This theorem is referenced by: ineq2 3345 dfss1 3354 in12 3361 in32 3362 in13 3363 in31 3364 inss2 3371 sslin 3376 inss 3380 indif1 3395 indifcom 3396 indir 3399 symdif1 3415 dfrab2 3425 0in 3473 disjr 3487 ssdifin0 3519 difdifdirss 3522 uneqdifeqim 3523 diftpsn3 3748 iunin1 3966 iinin1m 3971 riinm 3974 rintm 3994 inex2 4153 onintexmid 4587 resiun1 4941 dmres 4943 rescom 4947 resima2 4956 xpssres 4957 resindm 4964 resdmdfsn 4965 resopab 4966 imadisj 5005 ndmima 5020 intirr 5030 djudisj 5071 imainrect 5089 dmresv 5102 resdmres 5135 funimaexg 5316 fnresdisj 5342 fnimaeq0 5353 resasplitss 5411 f0rn0 5426 fvun2 5600 ressnop0 5714 fvsnun1 5730 fsnunfv 5734 offres 6155 smores3 6313 phplem2 6876 unfiin 6949 xpfi 6953 endjusym 7120 djucomen 7240 fzpreddisj 10096 fseq1p1m1 10119 hashunlem 10811 zfz1isolem1 10847 fprodsplit 11632 znnen 12444 setsfun 12542 setsfun0 12543 setsslid 12558 ressressg 12580 restin 14113 metreslem 14317 bdinex2 15089 |
Copyright terms: Public domain | W3C validator |