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

Theorem ssdisj 4458
Description: Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.) (Proof shortened by JJ, 14-Jul-2021.)
Assertion
Ref Expression
ssdisj ((𝐴𝐵 ∧ (𝐵𝐶) = ∅) → (𝐴𝐶) = ∅)

Proof of Theorem ssdisj
StepHypRef Expression
1 ssrin 4232 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 eqimss 4039 . . 3 ((𝐵𝐶) = ∅ → (𝐵𝐶) ⊆ ∅)
31, 2sylan9ss 3994 . 2 ((𝐴𝐵 ∧ (𝐵𝐶) = ∅) → (𝐴𝐶) ⊆ ∅)
4 ss0 4397 . 2 ((𝐴𝐶) ⊆ ∅ → (𝐴𝐶) = ∅)
53, 4syl 17 1 ((𝐴𝐵 ∧ (𝐵𝐶) = ∅) → (𝐴𝐶) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  cin 3946  wss 3947  c0 4321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322
This theorem is referenced by:  djudisj  6163  fimacnvdisj  6766  marypha1lem  9424  djuin  9909  ackbij1lem16  10226  ackbij1lem18  10228  fin23lem20  10328  fin23lem30  10333  elcls3  22578  neindisj  22612  imadifxp  31819  ldgenpisyslem1  33149  chtvalz  33629  pthhashvtx  34106  diophren  41536
  Copyright terms: Public domain W3C validator