Theorem ssdisj 4421

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

Step	Hyp	Ref	Expression
1		ssrin 4195	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		eqimss 3996	. . 3 ⊢ ((𝐵 ∩ 𝐶) = ∅ → (𝐵 ∩ 𝐶) ⊆ ∅)
3	1, 2	sylan9ss 3951	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) ⊆ ∅)
4		ss0 4360	. 2 ⊢ ((𝐴 ∩ 𝐶) ⊆ ∅ → (𝐴 ∩ 𝐶) = ∅)
5	3, 4	syl 18	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∩ cin 3905   ⊆ wss 3906  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-in 3913  df-ss 3923  df-nul 4288

This theorem is referenced by:  djudisj  6166  fimacnvdisj  6758  marypha1lem  9394  djuin  9905  ackbij1lem16  10218  ackbij1lem18  10220  fin23lem20  10322  fin23lem30  10327  psdmul  22310  elcls3  23221  neindisj  23255  imadifxp  32927  ldgenpisyslem1  34534  chtvalz  34997  pthhashvtx  35601  diophren  43523