Theorem ssdisj 4412

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∩ cin 3900   ⊆ wss 3901  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-in 3908  df-ss 3918  df-nul 4286

This theorem is referenced by:  djudisj  6125  fimacnvdisj  6712  marypha1lem  9336  djuin  9830  ackbij1lem16  10144  ackbij1lem18  10146  fin23lem20  10247  fin23lem30  10252  psdmul  22109  elcls3  23027  neindisj  23061  imadifxp  32676  ldgenpisyslem1  34320  chtvalz  34786  pthhashvtx  35322  diophren  43055