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

Theorem disj3 4454
Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
disj3 ((𝐴𝐵) = ∅ ↔ 𝐴 = (𝐴𝐵))

Proof of Theorem disj3
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 pm4.71 557 . . . 4 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
2 eldif 3961 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32bibi2i 337 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
41, 3bitr4i 278 . . 3 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐴𝐵)))
54albii 1819 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
6 disj1 4452 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
7 dfcleq 2730 . 2 (𝐴 = (𝐴𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
85, 6, 73bitr4i 303 1 ((𝐴𝐵) = ∅ ↔ 𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1538   = wceq 1540  wcel 2108  cdif 3948  cin 3950  c0 4333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-dif 3954  df-in 3958  df-nul 4334
This theorem is referenced by:  disjel  4457  disj4  4459  uneqdifeq  4493  difprsn1  4800  diftpsn3  4802  ssunsn2  4827  orddif  6480  php  9247  phpOLD  9259  hartogslem1  9582  infeq5i  9676  cantnfp1lem3  9720  dju1dif  10213  infdju1  10230  ssxr  11330  dprd2da  20062  dmdprdsplit2lem  20065  ablfac1eulem  20092  lbsextlem4  21163  opsrtoslem2  22080  alexsublem  24052  volun  25580  lhop1lem  26052  ex-dif  30442  difeq  32537  imadifxp  32614  disjdsct  32712  fzodif1  32794  carsgclctunlem1  34319  probun  34421  ballotlemfp1  34494  bj-disj2r  37029  topdifinfeq  37351  finixpnum  37612  lindsadd  37620  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem16  37643  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem27  37654  asindmre  37710  kelac2  43077  pwfi2f1o  43108  iccdifioo  45528  iccdifprioo  45529
  Copyright terms: Public domain W3C validator