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 3949	1 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ss 3922

This theorem is referenced by:  ssinss1d  4200  inss  4201  inindif  4331  disjdifg  4432  fipwuni  9382  ssfin4  10289  insubm  18872  distop  23152  fctop  23161  cctop  23163  ntrin  23218  innei  23282  lly1stc  23653  txcnp  23777  isfild  24015  utoptop  24391  restmetu  24727  lecmi  31954  mdslj2i  32672  mdslmd1lem1  32677  mdslmd1lem2  32678  elpwincl1  32871  pnfneige0  34341  inelcarsg  34701  ballotlemfrc  34917  bnj1177  35394  bnj1311  35412  cldbnd  36857  neiin  36863  ontgval  36962  mblfinlem4  38331  pmodlem1  40640  pmodlem2  40641  pmod1i  40642  pmod2iN  40643  pmodl42N  40645  dochdmj1  42184  redvmptabs  43141  ssficl  44315  ntrclskb  44815  ntrclsk13  44817  ntrneik3  44842  ntrneik13  44844  sswfaxreg  45716  icccncfext  46621  fourierdlem48  46888  fourierdlem49  46889  fourierdlem113  46953  caragendifcl  47248  omelesplit  47252  carageniuncllem2  47256  carageniuncl  47257