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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-ss 3916

This theorem is used by:  ssinss1d  4193  inss  4194  inindif  4324  disjdifg  4425  fipwuni  9397  ssfin4  10313  insubm  18928  distop  23221  fctop  23230  cctop  23232  ntrin  23287  innei  23351  lly1stc  23723  txcnp  23847  isfild  24085  utoptop  24461  restmetu  24797  lecmi  32084  mdslj2i  32802  mdslmd1lem1  32807  mdslmd1lem2  32808  elpwincl1  33001  pnfneige0  34462  inelcarsg  34823  ballotlemfrc  35039  bnj1177  35516  bnj1311  35534  cldbnd  36946  neiin  36952  ontgval  37051  mblfinlem4  38410  pmodlem1  40720  pmodlem2  40721  pmod1i  40722  pmod2iN  40723  pmodl42N  40725  dochdmj1  42264  redvmptabs  43236  ssficl  44410  ntrclskb  44910  ntrclsk13  44912  ntrneik3  44937  ntrneik13  44939  sswfaxreg  45811  icccncfext  46716  fourierdlem48  46983  fourierdlem49  46984  fourierdlem113  47048  caragendifcl  47343  omelesplit  47347  carageniuncllem2  47351  carageniuncl  47352