|   | 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 4449 | . 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) | |
| 2 | df-ral 3061 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1537 = wceq 1539 ∈ wcel 2107 ∀wral 3060 ∩ cin 3949 ∅c0 4332 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-dif 3953 df-in 3957 df-nul 4333 | 
| This theorem is referenced by: reldisj 4452 disj3 4453 undif4 4466 disjsn 4710 funun 6611 zfregs2 9774 dfac5lem4 10167 dfac5lem4OLD 10169 isf32lem9 10402 fzodisj 13734 fzodisjsn 13738 inpr0 32551 bnj1280 35035 ecin0 38354 zfregs2VD 44866 dfac5prim 45012 | 
| Copyright terms: Public domain | W3C validator |