![]() |
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 4260. Another version is given by dfin4 4268. (Contributed by NM, 10-Jun-2004.) |
Ref | Expression |
---|---|
dfin2 | ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3475 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | eldif 3957 | . . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | mpbiran 708 | . . . . 5 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ ¬ 𝑥 ∈ 𝐵) |
4 | 3 | con2bii 357 | . . . 4 ⊢ (𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ (V ∖ 𝐵)) |
5 | 4 | anbi2i 622 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵))) |
6 | eldif 3957 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵))) | |
7 | 5, 6 | bitr4i 278 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵))) |
8 | 7 | ineqri 4204 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 395 = wceq 1534 ∈ wcel 2099 Vcvv 3471 ∖ cdif 3944 ∩ cin 3946 |
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 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-dif 3950 df-in 3954 |
This theorem is referenced by: dfun3 4266 dfin3 4267 invdif 4269 difundi 4280 difindi 4282 difdif2 4287 |
Copyright terms: Public domain | W3C validator |