Theorem ssinss1 4145

Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
ssinss1	⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)

Proof of Theorem ssinss1

Step	Hyp	Ref	Expression
1		ssrin 4141	. 2 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐵))
2		inss1 4136	. 2 ⊢ (𝐶 ∩ 𝐵) ⊆ 𝐶
3	1, 2	sstrdi 3925	1 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   ∩ cin 4092

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-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  ssinss1d  4147  inss  4148  inindif  4327  disjdifg  4428  fipwuni  9455  ssfin4  10427  insubm  19064  distop  23368  fctop  23377  cctop  23379  ntrin  23434  innei  23498  lly1stc  23870  txcnp  23994  isfild  24232  utoptop  24608  restmetu  24944  lecmi  32261  mdslj2i  32979  mdslmd1lem1  32984  mdslmd1lem2  32985  elpwincl1  33220  pnfneige0  34694  inelcarsg  35054  ballotlemfrc  35270  bnj1177  35747  bnj1311  35765  cldbnd  37329  neiin  37335  ontgval  37434  mblfinlem4  38846  pmodlem1  41169  pmodlem2  41170  pmod1i  41171  pmod2iN  41172  pmodl42N  41174  dochdmj1  42713  redvmptabs  43677  ssficl  44831  ntrclskb  45330  ntrclsk13  45332  ntrneik3  45357  ntrneik13  45359  sswfaxreg  46241  icccncfext  47170  fourierdlem48  47437  fourierdlem49  47438  fourierdlem113  47502  caragendifcl  47797  omelesplit  47801  carageniuncllem2  47805  carageniuncl  47806