Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  disj1 Structured version   Visualization version   GIF version

Theorem disj1 4350
 Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.)
Assertion
Ref Expression
disj1 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem disj1
StepHypRef Expression
1 disj 4347 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
2 df-ral 3075 . 2 (∀𝑥𝐴 ¬ 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
31, 2bitri 278 1 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538   ∈ wcel 2111  ∀wral 3070   ∩ cin 3859  ∅c0 4227 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-dif 3863  df-in 3867  df-nul 4228 This theorem is referenced by:  reldisj  4351  reldisjOLD  4352  disj3  4353  undif4  4366  disjsn  4607  funun  6386  zfregs2  9221  dfac5lem4  9599  isf32lem9  9834  fzodisj  13133  fzodisjsn  13137  inpr0  30415  bnj1280  32532  ecin0  36080  zfregs2VD  41955
 Copyright terms: Public domain W3C validator