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 560 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) | |
2 | eldif 3945 | . . . . 5 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
3 | 2 | bibi2i 340 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))) |
4 | 1, 3 | bitr4i 280 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))) |
5 | 4 | albii 1816 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))) |
6 | disj1 4400 | . 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | |
7 | dfcleq 2815 | . 2 ⊢ (𝐴 = (𝐴 ∖ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))) | |
8 | 5, 6, 7 | 3bitr4i 305 | 1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1531 = wceq 1533 ∈ wcel 2110 ∖ cdif 3932 ∩ cin 3934 ∅c0 4290 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-v 3496 df-dif 3938 df-in 3942 df-nul 4291 |
This theorem is referenced by: disjel 4405 disj4 4407 uneqdifeq 4437 difprsn1 4726 diftpsn3 4728 ssunsn2 4753 orddif 6278 php 8695 hartogslem1 9000 infeq5i 9093 cantnfp1lem3 9137 dju1dif 9592 infdju1 9609 ssxr 10704 dprd2da 19158 dmdprdsplit2lem 19161 ablfac1eulem 19188 lbsextlem4 19927 opsrtoslem2 20259 alexsublem 22646 volun 24140 lhop1lem 24604 ex-dif 28196 difeq 30274 imadifxp 30345 disjdsct 30432 fzodif1 30510 carsgclctunlem1 31570 probun 31672 ballotlemfp1 31744 bj-disj2r 34335 topdifinfeq 34625 finixpnum 34871 lindsadd 34879 poimirlem11 34897 poimirlem12 34898 poimirlem13 34899 poimirlem14 34900 poimirlem16 34902 poimirlem18 34904 poimirlem21 34907 poimirlem22 34908 poimirlem27 34913 asindmre 34971 dffltz 39264 kelac2 39658 pwfi2f1o 39689 iccdifioo 41784 iccdifprioo 41785 |
Copyright terms: Public domain | W3C validator |