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

Theorem ssdisj 4407
 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 4208 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 eqimss 4021 . . 3 ((𝐵𝐶) = ∅ → (𝐵𝐶) ⊆ ∅)
31, 2sylan9ss 3978 . 2 ((𝐴𝐵 ∧ (𝐵𝐶) = ∅) → (𝐴𝐶) ⊆ ∅)
4 ss0 4350 . 2 ((𝐴𝐶) ⊆ ∅ → (𝐴𝐶) = ∅)
53, 4syl 17 1 ((𝐴𝐵 ∧ (𝐵𝐶) = ∅) → (𝐴𝐶) = ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531   ∩ cin 3933   ⊆ wss 3934  ∅c0 4289 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-dif 3937  df-in 3941  df-ss 3950  df-nul 4290 This theorem is referenced by:  djudisj  6017  fimacnvdisj  6550  marypha1lem  8889  djuin  9339  ackbij1lem16  9649  ackbij1lem18  9651  fin23lem20  9751  fin23lem30  9756  elcls3  21683  neindisj  21717  imadifxp  30343  ldgenpisyslem1  31415  chtvalz  31893  pthhashvtx  32367  diophren  39400
 Copyright terms: Public domain W3C validator