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

Theorem disj 4177
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 3738 . . . 4 (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
21eqeq1i 2769 . . 3 ((𝐴𝐵) = ∅ ↔ {𝑥 ∣ (𝑥𝐴𝑥𝐵)} = ∅)
3 abeq1 2875 . . 3 ({𝑥 ∣ (𝑥𝐴𝑥𝐵)} = ∅ ↔ ∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅))
4 imnan 388 . . . . 5 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
5 noel 4082 . . . . . 6 ¬ 𝑥 ∈ ∅
65nbn 363 . . . . 5 (¬ (𝑥𝐴𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅))
74, 6bitr2i 267 . . . 4 (((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥𝐴 → ¬ 𝑥𝐵))
87albii 1914 . . 3 (∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
92, 3, 83bitri 288 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
10 df-ral 3059 . 2 (∀𝑥𝐴 ¬ 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
119, 10bitr4i 269 1 ((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wal 1650   = wceq 1652  wcel 2155  {cab 2750  wral 3054  cin 3730  c0 4078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ral 3059  df-v 3351  df-dif 3734  df-in 3738  df-nul 4079
This theorem is referenced by:  disjr  4178  disj1  4179  disjne  4182  disjord  4797  disjiund  4799  otiunsndisj  5140  onxpdisj  6026  f0rn0  6271  onint  7192  zfreg  8706  kmlem4  9227  fin23lem30  9416  fin23lem31  9417  isf32lem3  9429  fpwwe2  9717  renfdisj  10351  fvinim0ffz  12794  s3iunsndisj  13995  metdsge  22930  2wspmdisj  27574  subfacp1lem1  31540  dfpo2  32021  dvmptfprodlem  40729  stoweidlem26  40812  stoweidlem59  40845  iundjiunlem  41245  otiunsndisjX  41960
  Copyright terms: Public domain W3C validator