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

Theorem disj1 4451
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 4449 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
2 df-ral 3061 . 2 (∀𝑥𝐴 ¬ 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
31, 2bitri 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