Theorem ssinss1 4194

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 4190	. 2 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐵))
2		inss1 4185	. 2 ⊢ (𝐶 ∩ 𝐵) ⊆ 𝐶
3	1, 2	sstrdi 3946	1 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∩ cin 3901   ⊆ wss 3902

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  ssinss1d  4196  inss  4197  inindif  4327  disjdifg  4428  fipwuni  9400  ssfin4  10316  insubm  18933  distop  23226  fctop  23235  cctop  23237  ntrin  23292  innei  23356  lly1stc  23728  txcnp  23852  isfild  24090  utoptop  24466  restmetu  24802  lecmi  32091  mdslj2i  32809  mdslmd1lem1  32814  mdslmd1lem2  32815  elpwincl1  33008  pnfneige0  34469  inelcarsg  34830  ballotlemfrc  35046  bnj1177  35523  bnj1311  35541  cldbnd  36953  neiin  36959  ontgval  37058  mblfinlem4  38417  pmodlem1  40727  pmodlem2  40728  pmod1i  40729  pmod2iN  40730  pmodl42N  40732  dochdmj1  42271  redvmptabs  43243  ssficl  44417  ntrclskb  44917  ntrclsk13  44919  ntrneik3  44944  ntrneik13  44946  sswfaxreg  45818  icccncfext  46723  fourierdlem48  46990  fourierdlem49  46991  fourierdlem113  47055  caragendifcl  47350  omelesplit  47354  carageniuncllem2  47358  carageniuncl  47359