![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfin2 | Structured version Visualization version GIF version |
Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 4224. Another version is given by dfin4 4232. (Contributed by NM, 10-Jun-2004.) |
Ref | Expression |
---|---|
dfin2 | ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3452 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | eldif 3925 | . . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | mpbiran 708 | . . . . 5 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ ¬ 𝑥 ∈ 𝐵) |
4 | 3 | con2bii 358 | . . . 4 ⊢ (𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ (V ∖ 𝐵)) |
5 | 4 | anbi2i 624 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵))) |
6 | eldif 3925 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵))) | |
7 | 5, 6 | bitr4i 278 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵))) |
8 | 7 | ineqri 4169 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 397 = wceq 1542 ∈ wcel 2107 Vcvv 3448 ∖ cdif 3912 ∩ cin 3914 |
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-v 3450 df-dif 3918 df-in 3922 |
This theorem is referenced by: dfun3 4230 dfin3 4231 invdif 4233 difundi 4244 difindi 4246 difdif2 4251 |
Copyright terms: Public domain | W3C validator |