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

Theorem reldisj 4458
Description: Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid ax-12 2174. (Revised by GG, 28-Jun-2024.)
Assertion
Ref Expression
reldisj (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))

Proof of Theorem reldisj
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ss 3979 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
2 eleq1w 2821 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
3 eleq1w 2821 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝐶𝑦𝐶))
42, 3imbi12d 344 . . . . . 6 (𝑥 = 𝑦 → ((𝑥𝐴𝑥𝐶) ↔ (𝑦𝐴𝑦𝐶)))
54spw 2030 . . . . 5 (∀𝑥(𝑥𝐴𝑥𝐶) → (𝑥𝐴𝑥𝐶))
6 pm5.44 542 . . . . . 6 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵))))
7 eldif 3972 . . . . . . 7 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
87imbi2i 336 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐶𝐵)) ↔ (𝑥𝐴 → (𝑥𝐶 ∧ ¬ 𝑥𝐵)))
96, 8bitr4di 289 . . . . 5 ((𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
105, 9syl 17 . . . 4 (∀𝑥(𝑥𝐴𝑥𝐶) → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
111, 10sylbi 217 . . 3 (𝐴𝐶 → ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ (𝑥𝐴𝑥 ∈ (𝐶𝐵))))
1211albidv 1917 . 2 (𝐴𝐶 → (∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵))))
13 disj1 4457 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
14 df-ss 3979 . 2 (𝐴 ⊆ (𝐶𝐵) ↔ ∀𝑥(𝑥𝐴𝑥 ∈ (𝐶𝐵)))
1512, 13, 143bitr4g 314 1 (𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1534   = wceq 1536  wcel 2105  cdif 3959  cin 3961  wss 3962  c0 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-v 3479  df-dif 3965  df-in 3969  df-ss 3979  df-nul 4339
This theorem is referenced by:  disj2  4463  ssdifsn  4792  oacomf1olem  8600  domdifsn  9092  elfiun  9467  cantnfp1lem3  9717  ssxr  11327  structcnvcnv  17186  fidomndrng  20790  elcls  23096  ist1-2  23370  nrmsep2  23379  nrmsep  23380  isnrm3  23382  isreg2  23400  hauscmplem  23429  connsub  23444  iunconnlem  23450  llycmpkgen2  23573  hausdiag  23668  trfil3  23911  isufil2  23931  filufint  23943  blcld  24533  i1fima2  25727  i1fd  25729  nbgrssvwo2  29393  pliguhgr  30514  symgcom2  33086  ssdifidlprm  33465  inunissunidif  37357  poimirlem15  37621  itg2addnclem2  37658  ntrk0kbimka  44028  ntrneicls11  44079  gneispace  44123  opndisj  48698  seposep  48721
  Copyright terms: Public domain W3C validator