Theorem ssinss1 4197

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

Syntax hints:   → wi 4   ∩ cin 3903   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-ss 3921

This theorem is referenced by:  ssinss1d  4199  inss  4200  inindif  4328  fipwuni  9372  ssfin4  10267  insubm  18852  distop  23055  fctop  23064  cctop  23066  ntrin  23121  innei  23185  lly1stc  23556  txcnp  23680  isfild  23918  utoptop  24294  restmetu  24630  lecmi  31805  mdslj2i  32523  mdslmd1lem1  32528  mdslmd1lem2  32529  elpwincl1  32724  pnfneige0  34248  inelcarsg  34608  ballotlemfrc  34824  bnj1177  35301  bnj1311  35319  cldbnd  36686  neiin  36692  ontgval  36791  mblfinlem4  38159  pmodlem1  40470  pmodlem2  40471  pmod1i  40472  pmod2iN  40473  pmodl42N  40475  dochdmj1  42014  redvmptabs  42969  ssficl  44145  ntrclskb  44645  ntrclsk13  44647  ntrneik3  44672  ntrneik13  44674  sswfaxreg  45563  icccncfext  46461  fourierdlem48  46728  fourierdlem49  46729  fourierdlem113  46793  caragendifcl  47088  omelesplit  47092  carageniuncllem2  47096  carageniuncl  47097