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

Theorem disj3 4216
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 554 . . . 4 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
2 eldif 3779 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32bibi2i 329 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
41, 3bitr4i 270 . . 3 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐴𝐵)))
54albii 1915 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
6 disj1 4214 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
7 dfcleq 2793 . 2 (𝐴 = (𝐴𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
85, 6, 73bitr4i 295 1 ((𝐴𝐵) = ∅ ↔ 𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  wal 1651   = wceq 1653  wcel 2157  cdif 3766  cin 3768  c0 4115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-v 3387  df-dif 3772  df-in 3776  df-nul 4116
This theorem is referenced by:  disjel  4219  disj4  4221  uneqdifeq  4251  difprsn1  4519  diftpsn3  4521  ssunsn2  4546  orddif  6034  php  8386  hartogslem1  8689  infeq5i  8783  cantnfp1lem3  8827  cda1dif  9286  infcda1  9303  ssxr  10397  dprd2da  18757  dmdprdsplit2lem  18760  ablfac1eulem  18787  lbsextlem4  19484  opsrtoslem2  19807  alexsublem  22176  volun  23653  lhop1lem  24117  ex-dif  27808  difeq  29873  imadifxp  29931  disjdsct  29998  carsgclctunlem1  30895  probun  30998  ballotlemfp1  31070  bj-disj2r  33505  topdifinfeq  33696  finixpnum  33883  poimirlem11  33909  poimirlem12  33910  poimirlem13  33911  poimirlem14  33912  poimirlem16  33914  poimirlem18  33916  poimirlem21  33919  poimirlem22  33920  poimirlem27  33925  asindmre  33983  kelac2  38420  pwfi2f1o  38451  iccdifioo  40486  iccdifprioo  40487
  Copyright terms: Public domain W3C validator