New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 437 | . . 3 | |
2 | elin 3219 | . . 3 | |
3 | elin 3219 | . . 3 | |
4 | 1, 2, 3 | 3bitr4i 268 | . 2 |
5 | 4 | eqriv 2350 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wa 358 wceq 1642 wcel 1710 cin 3208 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 |
This theorem is referenced by: ineq2 3451 dfss1 3460 in12 3466 in32 3467 in13 3468 in31 3469 inss2 3476 sslin 3481 inss 3484 indif1 3499 indifcom 3500 indir 3503 symdif1 3519 dfrab2 3530 disjr 3592 ssdifin0 3631 difdifdir 3637 uneqdifeq 3638 diftpsn3 3849 iinrab2 4029 iunin1 4031 iinin1 4037 riinn0 4040 rintn0 4056 compldif 4069 xpkexg 4288 dfiota4 4372 dfaddc2 4381 addccom 4406 nndisjeq 4429 phialllem2 4617 dmres 4986 rescom 4989 resabs1 4992 resopab 4999 imadisj 5015 ndmima 5025 intirr 5029 resdmres 5078 funun 5146 fnresdisj 5193 fvun2 5380 ressnop0 5436 fvsnun1 5447 enadj 6060 nchoicelem7 6295 nchoicelem14 6302 |
Copyright terms: Public domain | W3C validator |