| 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 3355 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 3 | elin 3355 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
| 4 | 1, 2, 3 | 3bitr4i 212 | . 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴)) |
| 5 | 4 | eqriv 2201 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
| Colors of variables: wff set class |
| Syntax hints: ∧ wa 104 = wceq 1372 ∈ wcel 2175 ∩ cin 3164 |
| 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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-v 2773 df-in 3171 |
| This theorem is referenced by: ineq2 3367 dfss1 3376 in12 3383 in32 3384 in13 3385 in31 3386 inss2 3393 sslin 3398 inss 3402 indif1 3417 indifcom 3418 indir 3421 symdif1 3437 dfrab2 3447 0in 3495 disjr 3509 ssdifin0 3541 difdifdirss 3544 uneqdifeqim 3545 diftpsn3 3773 iunin1 3991 iinin1m 3996 riinm 3999 rintm 4019 inex2 4178 onintexmid 4620 resiun1 4977 dmres 4979 rescom 4983 resima2 4992 xpssres 4993 resindm 5000 resdmdfsn 5001 resopab 5002 imadisj 5043 ndmima 5058 intirr 5068 djudisj 5109 imainrect 5127 dmresv 5140 resdmres 5173 funimaexg 5357 fnresdisj 5385 fnimaeq0 5396 resasplitss 5454 f0rn0 5469 fvun2 5645 ressnop0 5764 fvsnun1 5780 fsnunfv 5784 offres 6219 smores3 6378 phplem2 6949 unfiin 7022 xpfi 7028 endjusym 7197 djucomen 7327 fzpreddisj 10192 fseq1p1m1 10215 hashunlem 10947 zfz1isolem1 10983 fprodsplit 11879 znnen 12740 setsfun 12838 setsfun0 12839 setsslid 12854 ressressg 12878 restin 14619 metreslem 14823 perfectlem2 15443 bdinex2 15798 |
| Copyright terms: Public domain | W3C validator |