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

Theorem disj3 3972
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 659 . . . 4 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
2 eldif 3549 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32bibi2i 325 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
41, 3bitr4i 265 . . 3 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐴𝐵)))
54albii 1736 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
6 disj1 3970 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
7 dfcleq 2603 . 2 (𝐴 = (𝐴𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
85, 6, 73bitr4i 290 1 ((𝐴𝐵) = ∅ ↔ 𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  wal 1472   = wceq 1474  wcel 1976  cdif 3536  cin 3538  c0 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-v 3174  df-dif 3542  df-in 3546  df-nul 3874
This theorem is referenced by:  disjel  3974  disj4  3976  uneqdifeq  4008  uneqdifeqOLD  4009  difprsn1  4270  diftpsn3  4272  diftpsn3OLD  4273  ssunsn2  4296  orddif  5723  php  8007  hartogslem1  8308  infeq5i  8394  cantnfp1lem3  8438  cda1dif  8859  infcda1  8876  ssxr  9959  dprd2da  18213  dmdprdsplit2lem  18216  ablfac1eulem  18243  lbsextlem4  18931  opsrtoslem2  19255  alexsublem  21606  volun  23065  lhop1lem  23525  ex-dif  26466  difeq  28573  imadifxp  28630  disjdsct  28697  carsgclctunlem1  29540  probun  29642  ballotlemfp1  29714  topdifinfeq  32198  finixpnum  32388  poimirlem11  32414  poimirlem12  32415  poimirlem13  32416  poimirlem14  32417  poimirlem16  32419  poimirlem18  32421  poimirlem21  32424  poimirlem22  32425  poimirlem27  32430  asindmre  32489  kelac2  36477  pwfi2f1o  36508  iccdifioo  38412  iccdifprioo  38413
  Copyright terms: Public domain W3C validator