Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > incom | GIF 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 3229 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
3 | elin 3229 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
4 | 1, 2, 3 | 3bitr4i 211 | . 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴)) |
5 | 4 | eqriv 2114 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 = wceq 1316 ∈ wcel 1465 ∩ cin 3040 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 df-in 3047 |
This theorem is referenced by: ineq2 3241 dfss1 3250 in12 3257 in32 3258 in13 3259 in31 3260 inss2 3267 sslin 3272 inss 3276 indif1 3291 indifcom 3292 indir 3295 symdif1 3311 dfrab2 3321 0in 3368 disjr 3382 ssdifin0 3414 difdifdirss 3417 uneqdifeqim 3418 diftpsn3 3631 iunin1 3847 iinin1m 3852 riinm 3855 rintm 3875 inex2 4033 onintexmid 4457 resiun1 4808 dmres 4810 rescom 4814 resima2 4823 xpssres 4824 resindm 4831 resdmdfsn 4832 resopab 4833 imadisj 4871 ndmima 4886 intirr 4895 djudisj 4936 imainrect 4954 dmresv 4967 resdmres 5000 funimaexg 5177 fnresdisj 5203 fnimaeq0 5214 resasplitss 5272 f0rn0 5287 fvun2 5456 ressnop0 5569 fvsnun1 5585 fsnunfv 5589 offres 6001 smores3 6158 phplem2 6715 unfiin 6782 xpfi 6786 endjusym 6949 djucomen 7040 fzpreddisj 9819 fseq1p1m1 9842 hashunlem 10518 zfz1isolem1 10551 znnen 11838 setsfun 11921 setsfun0 11922 setsslid 11936 restin 12272 metreslem 12476 bdinex2 13025 |
Copyright terms: Public domain | W3C validator |