![]() |
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 266 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
2 | elin 3318 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
3 | elin 3318 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
4 | 1, 2, 3 | 3bitr4i 212 | . 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴)) |
5 | 4 | eqriv 2174 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 = wceq 1353 ∈ wcel 2148 ∩ cin 3128 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-in 3135 |
This theorem is referenced by: ineq2 3330 dfss1 3339 in12 3346 in32 3347 in13 3348 in31 3349 inss2 3356 sslin 3361 inss 3365 indif1 3380 indifcom 3381 indir 3384 symdif1 3400 dfrab2 3410 0in 3458 disjr 3472 ssdifin0 3504 difdifdirss 3507 uneqdifeqim 3508 diftpsn3 3733 iunin1 3951 iinin1m 3956 riinm 3959 rintm 3979 inex2 4138 onintexmid 4572 resiun1 4926 dmres 4928 rescom 4932 resima2 4941 xpssres 4942 resindm 4949 resdmdfsn 4950 resopab 4951 imadisj 4990 ndmima 5005 intirr 5015 djudisj 5056 imainrect 5074 dmresv 5087 resdmres 5120 funimaexg 5300 fnresdisj 5326 fnimaeq0 5337 resasplitss 5395 f0rn0 5410 fvun2 5583 ressnop0 5697 fvsnun1 5713 fsnunfv 5717 offres 6135 smores3 6293 phplem2 6852 unfiin 6924 xpfi 6928 endjusym 7094 djucomen 7214 fzpreddisj 10068 fseq1p1m1 10091 hashunlem 10779 zfz1isolem1 10815 fprodsplit 11600 znnen 12393 setsfun 12491 setsfun0 12492 setsslid 12507 ressressg 12528 restin 13569 metreslem 13773 bdinex2 14534 |
Copyright terms: Public domain | W3C validator |