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

Theorem ssdisj 4460
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 4234 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 eqimss 4041 . . 3 ((𝐵𝐶) = ∅ → (𝐵𝐶) ⊆ ∅)
31, 2sylan9ss 3996 . 2 ((𝐴𝐵 ∧ (𝐵𝐶) = ∅) → (𝐴𝐶) ⊆ ∅)
4 ss0 4399 . 2 ((𝐴𝐶) ⊆ ∅ → (𝐴𝐶) = ∅)
53, 4syl 17 1 ((𝐴𝐵 ∧ (𝐵𝐶) = ∅) → (𝐴𝐶) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  cin 3948  wss 3949  c0 4323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324
This theorem is referenced by:  djudisj  6167  fimacnvdisj  6770  marypha1lem  9428  djuin  9913  ackbij1lem16  10230  ackbij1lem18  10232  fin23lem20  10332  fin23lem30  10337  elcls3  22587  neindisj  22621  imadifxp  31832  ldgenpisyslem1  33161  chtvalz  33641  pthhashvtx  34118  diophren  41551
  Copyright terms: Public domain W3C validator