Theorem ssinss1 4198

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

This proof depends on syntax axioms:   → wi 4   ∩ cin 3905   ⊆ wss 3906

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ss 3923

This theorem is used by:  ssinss1d  4200  inss  4201  inindif  4331  disjdifg  4432  fipwuni  9393  ssfin4  10309  insubm  18916  distop  23204  fctop  23213  cctop  23215  ntrin  23270  innei  23334  lly1stc  23706  txcnp  23830  isfild  24068  utoptop  24444  restmetu  24780  lecmi  32027  mdslj2i  32745  mdslmd1lem1  32750  mdslmd1lem2  32751  elpwincl1  32944  pnfneige0  34407  inelcarsg  34768  ballotlemfrc  34984  bnj1177  35461  bnj1311  35479  cldbnd  36896  neiin  36902  ontgval  37001  mblfinlem4  38370  pmodlem1  40680  pmodlem2  40681  pmod1i  40682  pmod2iN  40683  pmodl42N  40685  dochdmj1  42224  redvmptabs  43181  ssficl  44355  ntrclskb  44855  ntrclsk13  44857  ntrneik3  44882  ntrneik13  44884  sswfaxreg  45756  icccncfext  46661  fourierdlem48  46928  fourierdlem49  46929  fourierdlem113  46993  caragendifcl  47288  omelesplit  47292  carageniuncllem2  47296  carageniuncl  47297