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

Theorem disj3 4455
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 556 . . . 4 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
2 eldif 3954 . . . . 5 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵))
32bibi2i 336 . . . 4 ((𝑥𝐴𝑥 ∈ (𝐴𝐵)) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐵)))
41, 3bitr4i 277 . . 3 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐴𝐵)))
54albii 1813 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
6 disj1 4452 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
7 dfcleq 2718 . 2 (𝐴 = (𝐴𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐴𝐵)))
85, 6, 73bitr4i 302 1 ((𝐴𝐵) = ∅ ↔ 𝐴 = (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wal 1531   = wceq 1533  wcel 2098  cdif 3941  cin 3943  c0 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-dif 3947  df-in 3951  df-nul 4323
This theorem is referenced by:  disjel  4458  disj4  4460  uneqdifeq  4494  difprsn1  4805  diftpsn3  4807  ssunsn2  4832  orddif  6467  php  9235  phpOLD  9247  hartogslem1  9567  infeq5i  9661  cantnfp1lem3  9705  dju1dif  10197  infdju1  10214  ssxr  11315  dprd2da  20011  dmdprdsplit2lem  20014  ablfac1eulem  20041  lbsextlem4  21061  opsrtoslem2  22022  alexsublem  23992  volun  25518  lhop1lem  25990  ex-dif  30305  difeq  32394  imadifxp  32470  disjdsct  32564  fzodif1  32643  carsgclctunlem1  34065  probun  34167  ballotlemfp1  34239  bj-disj2r  36635  topdifinfeq  36957  finixpnum  37206  lindsadd  37214  poimirlem11  37232  poimirlem12  37233  poimirlem13  37234  poimirlem14  37235  poimirlem16  37237  poimirlem18  37239  poimirlem21  37242  poimirlem22  37243  poimirlem27  37248  asindmre  37304  kelac2  42628  pwfi2f1o  42659  iccdifioo  45035  iccdifprioo  45036
  Copyright terms: Public domain W3C validator