Theorem ssinss1 4141

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3896   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-in 4090

This theorem is used by:  ssinss1d  4143  inss  4144  inindif  4323  disjdifg  4424  fipwuni  9425  ssfin4  10395  insubm  19023  distop  23322  fctop  23331  cctop  23333  ntrin  23388  innei  23452  lly1stc  23824  txcnp  23948  isfild  24186  utoptop  24562  restmetu  24898  lecmi  32213  mdslj2i  32931  mdslmd1lem1  32936  mdslmd1lem2  32937  elpwincl1  33172  pnfneige0  34633  inelcarsg  34993  ballotlemfrc  35209  bnj1177  35686  bnj1311  35704  cldbnd  37238  neiin  37244  ontgval  37343  mblfinlem4  38715  pmodlem1  41040  pmodlem2  41041  pmod1i  41042  pmod2iN  41043  pmodl42N  41045  dochdmj1  42584  redvmptabs  43548  ssficl  44707  ntrclskb  45206  ntrclsk13  45208  ntrneik3  45233  ntrneik13  45235  sswfaxreg  46113  icccncfext  47033  fourierdlem48  47300  fourierdlem49  47301  fourierdlem113  47365  caragendifcl  47660  omelesplit  47664  carageniuncllem2  47668  carageniuncl  47669