Theorem ssinss1 4206

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

Syntax hints:   → wi 4   ∩ cin 3912   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ss 3930

This theorem is referenced by:  ssinss1d  4208  inss  4209  inindif  4338  fipwuni  9386  ssfin4  10294  insubm  18877  distop  23121  fctop  23130  cctop  23132  ntrin  23187  innei  23251  lly1stc  23622  txcnp  23746  isfild  23984  utoptop  24360  restmetu  24696  lecmi  31895  mdslj2i  32613  mdslmd1lem1  32618  mdslmd1lem2  32619  elpwincl1  32812  pnfneige0  34286  inelcarsg  34646  ballotlemfrc  34862  bnj1177  35339  bnj1311  35357  cldbnd  36726  neiin  36732  ontgval  36831  mblfinlem4  38199  pmodlem1  40510  pmodlem2  40511  pmod1i  40512  pmod2iN  40513  pmodl42N  40515  dochdmj1  42054  redvmptabs  43011  ssficl  44187  ntrclskb  44687  ntrclsk13  44689  ntrneik3  44714  ntrneik13  44716  sswfaxreg  45588  icccncfext  46493  fourierdlem48  46760  fourierdlem49  46761  fourierdlem113  46825  caragendifcl  47120  omelesplit  47124  carageniuncllem2  47128  carageniuncl  47129