Theorem ssinss1 4191

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

This proof depends on syntax axioms:   → wi 4   ∩ cin 3898   ⊆ wss 3899

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  ssinss1d  4193  inss  4194  inindif  4324  disjdifg  4425  fipwuni  9418  ssfin4  10388  insubm  19014  distop  23313  fctop  23322  cctop  23324  ntrin  23379  innei  23443  lly1stc  23815  txcnp  23939  isfild  24177  utoptop  24553  restmetu  24889  lecmi  32204  mdslj2i  32922  mdslmd1lem1  32927  mdslmd1lem2  32928  elpwincl1  33121  pnfneige0  34583  inelcarsg  34943  ballotlemfrc  35159  bnj1177  35636  bnj1311  35654  cldbnd  37114  neiin  37120  ontgval  37219  mblfinlem4  38578  pmodlem1  40903  pmodlem2  40904  pmod1i  40905  pmod2iN  40906  pmodl42N  40908  dochdmj1  42447  redvmptabs  43411  ssficl  44569  ntrclskb  45068  ntrclsk13  45070  ntrneik3  45095  ntrneik13  45097  sswfaxreg  45976  icccncfext  46896  fourierdlem48  47163  fourierdlem49  47164  fourierdlem113  47228  caragendifcl  47523  omelesplit  47527  carageniuncllem2  47531  carageniuncl  47532