![]() |
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 4008. Another version is given by dfin4 4016. (Contributed by NM, 10-Jun-2004.) |
Ref | Expression |
---|---|
dfin2 | ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3354 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | eldif 3733 | . . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 1, 2 | mpbiran 688 | . . . . 5 ⊢ (𝑥 ∈ (V ∖ 𝐵) ↔ ¬ 𝑥 ∈ 𝐵) |
4 | 3 | con2bii 346 | . . . 4 ⊢ (𝑥 ∈ 𝐵 ↔ ¬ 𝑥 ∈ (V ∖ 𝐵)) |
5 | 4 | anbi2i 609 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵))) |
6 | eldif 3733 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (V ∖ 𝐵))) | |
7 | 5, 6 | bitr4i 267 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (𝐴 ∖ (V ∖ 𝐵))) |
8 | 7 | ineqri 3957 | 1 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (V ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 382 = wceq 1631 ∈ wcel 2145 Vcvv 3351 ∖ cdif 3720 ∩ cin 3722 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-dif 3726 df-in 3730 |
This theorem is referenced by: dfun3 4014 dfin3 4015 invdif 4017 difundi 4028 difindi 4030 difdif2 4033 |
Copyright terms: Public domain | W3C validator |