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

Theorem disj 4402
Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.)
Assertion
Ref Expression
disj ((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem disj
StepHypRef Expression
1 df-in 3947 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
21eqeq1i 2831 . . 3 ((𝐴𝐵) = ∅ ↔ {𝑥 ∣ (𝑥𝐴𝑥𝐵)} = ∅)
3 abeq1 2951 . . 3 ({𝑥 ∣ (𝑥𝐴𝑥𝐵)} = ∅ ↔ ∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅))
4 imnan 400 . . . . 5 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
5 noel 4300 . . . . . 6 ¬ 𝑥 ∈ ∅
65nbn 374 . . . . 5 (¬ (𝑥𝐴𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅))
74, 6bitr2i 277 . . . 4 (((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥𝐴 → ¬ 𝑥𝐵))
87albii 1813 . . 3 (∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
92, 3, 83bitri 298 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
10 df-ral 3148 . 2 (∀𝑥𝐴 ¬ 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
119, 10bitr4i 279 1 ((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1528   = wceq 1530  wcel 2107  {cab 2804  wral 3143  cin 3939  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-ral 3148  df-dif 3943  df-in 3947  df-nul 4296
This theorem is referenced by:  disjr  4403  disj1  4404  disjne  4407  disjord  5051  disjiund  5053  otiunsndisj  5407  onxpdisj  6308  f0rn0  6561  onint  7498  zfreg  9048  kmlem4  9568  fin23lem30  9753  fin23lem31  9754  isf32lem3  9766  fpwwe2  10054  renfdisj  10690  fvinim0ffz  13146  s3iunsndisj  14318  metdsge  23375  2wspmdisj  28033  subfacp1lem1  32313  dfpo2  32878  dvmptfprodlem  42097  stoweidlem26  42180  stoweidlem59  42213  iundjiunlem  42610  otiunsndisjX  43347
  Copyright terms: Public domain W3C validator