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 253 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
2 | elin 3126 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
3 | elin 3126 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | |
4 | 1, 2, 3 | 3bitr4i 201 | . 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴)) |
5 | 4 | eqriv 2037 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 97 = wceq 1243 ∈ wcel 1393 ∩ cin 2916 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-v 2559 df-in 2924 |
This theorem is referenced by: ineq2 3132 dfss1 3141 in12 3148 in32 3149 in13 3150 in31 3151 inss2 3158 sslin 3163 inss 3166 indif1 3182 indifcom 3183 indir 3186 symdif1 3202 dfrab2 3212 disjr 3269 ssdifin0 3304 difdifdirss 3307 uneqdifeqim 3308 diftpsn3 3505 iunin1 3721 iinin1m 3726 riinm 3729 rintm 3744 inex2 3892 onintexmid 4297 resiun1 4630 dmres 4632 rescom 4636 resima2 4644 xpssres 4645 resopab 4652 imadisj 4687 ndmima 4702 intirr 4711 djudisj 4750 imainrect 4766 dmresv 4779 resdmres 4812 funimaexg 4983 fnresdisj 5009 fnimaeq0 5020 resasplitss 5069 fvun2 5240 ressnop0 5344 fvsnun1 5360 fsnunfv 5363 offres 5762 smores3 5908 phplem2 6316 fzpreddisj 8933 fseq1p1m1 8956 bdinex2 10020 |
Copyright terms: Public domain | W3C validator |