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 264 | . . 3 | |
2 | elin 3259 | . . 3 | |
3 | elin 3259 | . . 3 | |
4 | 1, 2, 3 | 3bitr4i 211 | . 2 |
5 | 4 | eqriv 2136 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wceq 1331 wcel 1480 cin 3070 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-in 3077 |
This theorem is referenced by: ineq2 3271 dfss1 3280 in12 3287 in32 3288 in13 3289 in31 3290 inss2 3297 sslin 3302 inss 3306 indif1 3321 indifcom 3322 indir 3325 symdif1 3341 dfrab2 3351 0in 3398 disjr 3412 ssdifin0 3444 difdifdirss 3447 uneqdifeqim 3448 diftpsn3 3661 iunin1 3877 iinin1m 3882 riinm 3885 rintm 3905 inex2 4063 onintexmid 4487 resiun1 4838 dmres 4840 rescom 4844 resima2 4853 xpssres 4854 resindm 4861 resdmdfsn 4862 resopab 4863 imadisj 4901 ndmima 4916 intirr 4925 djudisj 4966 imainrect 4984 dmresv 4997 resdmres 5030 funimaexg 5207 fnresdisj 5233 fnimaeq0 5244 resasplitss 5302 f0rn0 5317 fvun2 5488 ressnop0 5601 fvsnun1 5617 fsnunfv 5621 offres 6033 smores3 6190 phplem2 6747 unfiin 6814 xpfi 6818 endjusym 6981 djucomen 7072 fzpreddisj 9851 fseq1p1m1 9874 hashunlem 10550 zfz1isolem1 10583 znnen 11911 setsfun 11994 setsfun0 11995 setsslid 12009 restin 12345 metreslem 12549 bdinex2 13098 |
Copyright terms: Public domain | W3C validator |