Theorem ssdisj 4416

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 4141	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		eqimss 3971	. . 3 ⊢ ((𝐵 ∩ 𝐶) = ∅ → (𝐵 ∩ 𝐶) ⊆ ∅)
3	1, 2	sylan9ss 3926	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) ⊆ ∅)
4		ss0 4355	. 2 ⊢ ((𝐴 ∩ 𝐶) ⊆ ∅ → (𝐴 ∩ 𝐶) = ∅)
5	3, 4	syl 18	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ 𝐶) = ∅) → (𝐴 ∩ 𝐶) = ∅)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3900   ∩ cin 4092  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-nul 4282

This theorem is used by:  djudisj  6171  fimacnvdisj  6785  marypha1lem  9455  djuin  10029  ackbij1lem16  10342  ackbij1lem18  10344  fin23lem20  10445  fin23lem30  10450  psdmul  22520  elcls3  23434  neindisj  23468  pthhashvtx  30348  imadifxp  33270  ldgenpisyslem1  34879  chtvalz  35341  diophren  44024