![]() |
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 4193 | . . 3 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
2 | dfss4 4223 | . . 3 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵)) | |
3 | 1, 2 | mpbi 229 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∩ 𝐵) |
4 | difin 4226 | . . 3 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) | |
5 | 4 | difeq2i 4084 | . 2 ⊢ (𝐴 ∖ (𝐴 ∖ (𝐴 ∩ 𝐵))) = (𝐴 ∖ (𝐴 ∖ 𝐵)) |
6 | 3, 5 | eqtr3i 2767 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∖ cdif 3912 ∩ cin 3914 ⊆ wss 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-in 3922 df-ss 3932 |
This theorem is referenced by: indif 4234 cnvin 6102 imain 6591 resin 6811 elcls 22440 cmmbl 24914 mbfeqalem2 25022 itg1addlem4 25079 itg1addlem4OLD 25080 itg1addlem5 25081 suppovss 31640 inelsiga 32774 inelros 32812 topdifinffinlem 35847 poimirlem9 36116 mblfinlem4 36147 ismblfin 36148 cnambfre 36155 stoweidlem50 44365 saliinclf 44641 sge0fodjrnlem 44731 meadjiunlem 44780 caragendifcl 44829 |
Copyright terms: Public domain | W3C validator |