Theorem ssdisj 4440

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 4222	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		eqimss 4022	. . 3 ⊢ ((𝐵 ∩ 𝐶) = ∅ → (𝐵 ∩ 𝐶) ⊆ ∅)
3	1, 2	sylan9ss 3977	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) ⊆ ∅)
4		ss0 4382	. 2 ⊢ ((𝐴 ∩ 𝐶) ⊆ ∅ → (𝐴 ∩ 𝐶) = ∅)
5	3, 4	syl 17	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-in 3938  df-ss 3948  df-nul 4314

This theorem is referenced by:  djudisj  6161  fimacnvdisj  6761  marypha1lem  9450  djuin  9937  ackbij1lem16  10253  ackbij1lem18  10255  fin23lem20  10356  fin23lem30  10361  psdmul  22109  elcls3  23026  neindisj  23060  imadifxp  32587  ldgenpisyslem1  34199  chtvalz  34666  pthhashvtx  35155  diophren  42811