| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > dfin4 | Structured version Visualization version GIF version | ||
| Description: Alternate definition of the intersection of two classes. Exercise 4.10(q) of [Mendelson] p. 231. (Contributed by NM, 25-Nov-2003.) |
| Ref | Expression |
|---|---|
| dfin4 | ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inss1 4237 | . . 3 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
| 2 | dfss4 4269 | . . 3 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵)) | |
| 3 | 1, 2 | mpbi 230 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵) |
| 4 | difin 4272 | . . 3 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) | |
| 5 | 4 | difeq2i 4123 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∖ (𝐴 ∖ 𝐵)) |
| 6 | 3, 5 | eqtr3i 2767 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∖ cdif 3948 ∩ cin 3950 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-in 3958 df-ss 3968 |
| This theorem is referenced by: indif 4280 cnvin 6164 imain 6651 resin 6870 elcls 23081 cmmbl 25569 mbfeqalem2 25677 itg1addlem4 25734 itg1addlem5 25735 suppovss 32690 inelsiga 34136 inelros 34174 topdifinffinlem 37348 poimirlem9 37636 mblfinlem4 37667 ismblfin 37668 cnambfre 37675 stoweidlem50 46065 saliinclf 46341 sge0fodjrnlem 46431 meadjiunlem 46480 caragendifcl 46529 |
| Copyright terms: Public domain | W3C validator |