Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > disj | Structured version Visualization version GIF version |
Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) |
Ref | Expression |
---|---|
disj | ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-in 3942 | . . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
2 | 1 | eqeq1i 2826 | . . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = ∅) |
3 | abeq1 2946 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅)) | |
4 | imnan 400 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
5 | noel 4295 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
6 | 5 | nbn 374 | . . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅)) |
7 | 4, 6 | bitr2i 277 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
8 | 7 | albii 1811 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
9 | 2, 3, 8 | 3bitri 298 | . 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
10 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | |
11 | 9, 10 | bitr4i 279 | 1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∀wal 1526 = wceq 1528 ∈ wcel 2105 {cab 2799 ∀wral 3138 ∩ cin 3934 ∅c0 4290 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-ral 3143 df-dif 3938 df-in 3942 df-nul 4291 |
This theorem is referenced by: disjr 4398 disj1 4399 disjne 4402 disjord 5046 disjiund 5048 otiunsndisj 5402 onxpdisj 6304 f0rn0 6558 onint 7498 zfreg 9048 kmlem4 9568 fin23lem30 9753 fin23lem31 9754 isf32lem3 9766 fpwwe2 10054 renfdisj 10690 fvinim0ffz 13146 s3iunsndisj 14318 metdsge 23386 2wspmdisj 28044 subfacp1lem1 32324 dfpo2 32889 dvmptfprodlem 42109 stoweidlem26 42192 stoweidlem59 42225 iundjiunlem 42622 otiunsndisjX 43359 |
Copyright terms: Public domain | W3C validator |