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 3581 | . . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
2 | 1 | eqeq1i 2627 | . . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = ∅) |
3 | abeq1 2733 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = ∅ ↔ ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅)) | |
4 | imnan 438 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
5 | noel 3919 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
6 | 5 | nbn 362 | . . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅)) |
7 | 4, 6 | bitr2i 265 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
8 | 7 | albii 1747 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
9 | 2, 3, 8 | 3bitri 286 | . 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
10 | df-ral 2917 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | |
11 | 9, 10 | bitr4i 267 | 1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∀wal 1481 = wceq 1483 ∈ wcel 1990 {cab 2608 ∀wral 2912 ∩ cin 3573 ∅c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-v 3202 df-dif 3577 df-in 3581 df-nul 3916 |
This theorem is referenced by: disjr 4018 disj1 4019 disjne 4022 disjord 4641 disjiund 4643 otiunsndisj 4980 onxpdisj 5847 f0rn0 6090 onint 6995 zfreg 8500 zfregOLD 8502 kmlem4 8975 fin23lem30 9164 fin23lem31 9165 isf32lem3 9177 fpwwe2 9465 renfdisj 10098 fvinim0ffz 12587 s3iunsndisj 13707 metdsge 22652 2wspmdisj 27201 subfacp1lem1 31161 dfpo2 31645 dvmptfprodlem 40159 stoweidlem26 40243 stoweidlem59 40276 iundjiunlem 40676 otiunsndisjX 41298 |
Copyright terms: Public domain | W3C validator |