| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > disj1 | Structured version Visualization version GIF version | ||
| Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.) |
| Ref | Expression |
|---|---|
| disj1 | ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | disj 4402 | . 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | |
| 2 | df-ral 3052 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1539 = wceq 1541 ∈ wcel 2113 ∀wral 3051 ∩ cin 3900 ∅c0 4285 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-ral 3052 df-dif 3904 df-in 3908 df-nul 4286 |
| This theorem is referenced by: reldisj 4405 disj3 4406 undif4 4419 disjsn 4668 funun 6538 zfregs2 9642 dfac5lem4 10036 dfac5lem4OLD 10038 isf32lem9 10271 fzodisj 13609 fzodisjsn 13613 inpr0 32607 bnj1280 35176 axregszf 35285 ecin0 38545 zfregs2VD 45081 dfac5prim 45231 permac8prim 45255 |
| Copyright terms: Public domain | W3C validator |