Theorem ssinss1 3841

Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)

Assertion

Ref	Expression
ssinss1	|- ( A C_ C -> ( A i^i B ) C_ C )

Proof of Theorem ssinss1

Step	Hyp	Ref	Expression
1		inss1 3833	. 2 |- ( A i^i B ) C_ A
2		sstr2 3610	. 2 |- ( ( A i^i B ) C_ A -> ( A C_ C -> ( A i^i B ) C_ C ) )
3	1, 2	ax-mp 5	1 |- ( A C_ C -> ( A i^i B ) C_ C )

Syntax hints:   -> wi 4   i^i cin 3573   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  inss  3842  wfrlem4  7418  wfrlem5  7419  fipwuni  8332  ssfin4  9132  distop  20799  fctop  20808  cctop  20810  ntrin  20865  innei  20929  lly1stc  21299  txcnp  21423  isfild  21662  utoptop  22038  restmetu  22375  lecmi  28461  mdslj2i  29179  mdslmd1lem1  29184  mdslmd1lem2  29185  elpwincl1  29357  pnfneige0  29997  inelcarsg  30373  ballotlemfrc  30588  bnj1177  31074  bnj1311  31092  frrlem4  31783  frrlem5  31784  cldbnd  32321  neiin  32327  ontgval  32430  mblfinlem4  33449  pmodlem1  35132  pmodlem2  35133  pmod1i  35134  pmod2iN  35135  pmodl42N  35137  dochdmj1  36679  ssficl  37874  ntrclskb  38367  ntrclsk13  38369  ntrneik3  38394  ntrneik13  38396  ssinss1d  39214  icccncfext  40100  fourierdlem48  40371  fourierdlem49  40372  fourierdlem113  40436  caragendifcl  40728  omelesplit  40732  carageniuncllem2  40736  carageniuncl  40737