![]() |
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 4230 | . . 3 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
2 | dfss4 4260 | . . 3 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵)) | |
3 | 1, 2 | mpbi 229 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵) |
4 | difin 4263 | . . 3 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) | |
5 | 4 | difeq2i 4118 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∖ (𝐴 ∖ 𝐵)) |
6 | 3, 5 | eqtr3i 2756 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∖ cdif 3944 ∩ cin 3946 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-in 3954 df-ss 3964 |
This theorem is referenced by: indif 4271 cnvin 6156 imain 6644 resin 6865 elcls 23068 cmmbl 25554 mbfeqalem2 25662 itg1addlem4 25719 itg1addlem4OLD 25720 itg1addlem5 25721 suppovss 32597 inelsiga 33968 inelros 34006 topdifinffinlem 37054 poimirlem9 37330 mblfinlem4 37361 ismblfin 37362 cnambfre 37369 stoweidlem50 45671 saliinclf 45947 sge0fodjrnlem 46037 meadjiunlem 46086 caragendifcl 46135 |
Copyright terms: Public domain | W3C validator |