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

Theorem disj3 4164
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 665 . . . 4 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
2 eldif 3725 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32bibi2i 326 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
41, 3bitr4i 267 . . 3 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐴𝐵)))
54albii 1896 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
6 disj1 4162 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
7 dfcleq 2754 . 2 (𝐴 = (𝐴𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
85, 6, 73bitr4i 292 1 ((𝐴𝐵) = ∅ ↔ 𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wal 1630   = wceq 1632  wcel 2139  cdif 3712  cin 3714  c0 4058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-v 3342  df-dif 3718  df-in 3722  df-nul 4059
This theorem is referenced by:  disjel  4167  disj4  4169  uneqdifeq  4201  uneqdifeqOLD  4202  difprsn1  4475  diftpsn3  4477  diftpsn3OLD  4478  ssunsn2  4504  orddif  5981  php  8311  hartogslem1  8614  infeq5i  8708  cantnfp1lem3  8752  cda1dif  9210  infcda1  9227  ssxr  10319  dprd2da  18661  dmdprdsplit2lem  18664  ablfac1eulem  18691  lbsextlem4  19383  opsrtoslem2  19707  alexsublem  22069  volun  23533  lhop1lem  23995  ex-dif  27612  difeq  29683  imadifxp  29742  disjdsct  29810  carsgclctunlem1  30709  probun  30811  ballotlemfp1  30883  bj-disj2r  33337  topdifinfeq  33527  finixpnum  33725  poimirlem11  33751  poimirlem12  33752  poimirlem13  33753  poimirlem14  33754  poimirlem16  33756  poimirlem18  33758  poimirlem21  33761  poimirlem22  33762  poimirlem27  33767  asindmre  33826  kelac2  38155  pwfi2f1o  38186  iccdifioo  40262  iccdifprioo  40263
  Copyright terms: Public domain W3C validator