| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > disj3 | Structured version Visualization version GIF version | ||
| Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.) |
| Ref | Expression |
|---|---|
| disj3 | ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm4.71 557 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
| 2 | eldif 3961 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
| 3 | 2 | bibi2i 337 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
| 4 | 1, 3 | bitr4i 278 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))) |
| 5 | 4 | albii 1819 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))) |
| 6 | disj1 4452 | . 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | |
| 7 | dfcleq 2730 | . 2 ⊢ (𝐴 = (𝐴 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))) | |
| 8 | 5, 6, 7 | 3bitr4i 303 | 1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 = wceq 1540 ∈ wcel 2108 ∖ cdif 3948 ∩ cin 3950 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-v 3482 df-dif 3954 df-in 3958 df-nul 4334 |
| This theorem is referenced by: disjel 4457 disj4 4459 uneqdifeq 4493 difprsn1 4800 diftpsn3 4802 ssunsn2 4827 orddif 6480 php 9247 phpOLD 9259 hartogslem1 9582 infeq5i 9676 cantnfp1lem3 9720 dju1dif 10213 infdju1 10230 ssxr 11330 dprd2da 20062 dmdprdsplit2lem 20065 ablfac1eulem 20092 lbsextlem4 21163 opsrtoslem2 22080 alexsublem 24052 volun 25580 lhop1lem 26052 ex-dif 30442 difeq 32537 imadifxp 32614 disjdsct 32712 fzodif1 32794 carsgclctunlem1 34319 probun 34421 ballotlemfp1 34494 bj-disj2r 37029 topdifinfeq 37351 finixpnum 37612 lindsadd 37620 poimirlem11 37638 poimirlem12 37639 poimirlem13 37640 poimirlem14 37641 poimirlem16 37643 poimirlem18 37645 poimirlem21 37648 poimirlem22 37649 poimirlem27 37654 asindmre 37710 kelac2 43077 pwfi2f1o 43108 iccdifioo 45528 iccdifprioo 45529 |
| Copyright terms: Public domain | W3C validator |