Theorem inss2 3718

Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)

Assertion

Ref	Expression
inss2

Proof of Theorem inss2

Step	Hyp	Ref	Expression
1		incom 3690	. 2
2		inss1 3717	. 2
3	1, 2	eqsstr3i 3534	1

Syntax hints:  i^icin 3474  C_wss 3475

This theorem is referenced by:  difin0  3901  ordin  4913  onfr  4922  ordelinel  4981  relin2  5126  relres  5306  ssrnres  5450  cnvcnv  5464  fnresin2  5701  fresaunres2  5762  ssimaex  5938  exfo  6049  ffvresb  6062  ofrfval  6548  ofval  6549  ofrval  6550  off  6554  ofres  6555  ofco  6560  offres  6795  fnwelem  6915  fnse  6917  tpostpos  6994  smores3  7043  tfrlem5  7068  erinxp  7404  pmresg  7466  nnfi  7730  ixpfi2  7838  f1opwfi  7844  dffi2  7903  elfiun  7910  marypha1lem  7913  ordtypelem3  7966  ordtypelem6  7969  ordtypelem7  7970  hartogslem1  7988  unxpwdom  8036  epfrs  8183  tcmin  8193  bnd2  8332  tskwe  8352  r0weon  8411  infxpenlem  8412  fodomfi2  8462  infpwfien  8464  cdainf  8593  ackbij1lem6  8626  ackbij1lem9  8629  ackbij1lem10  8630  ackbij1lem11  8631  ackbij1lem15  8635  ackbij1lem16  8636  ackbij1lem18  8638  ackbij1b  8640  sdom2en01  8703  fin23lem26  8726  fin23lem13  8733  isfin1-3  8787  fin56  8794  fin1a2lem9  8809  ttukeylem6  8915  brdom3  8927  brdom5  8928  brdom4  8929  fpwwe2lem8  9036  fpwwe2lem9  9037  fpwwe2lem12  9040  fpwwe2  9042  canthwelem  9049  gruima  9201  ingru  9214  gruina  9217  grur1a  9218  ltrelpi  9288  ltrelnq  9325  nqerf  9329  dedekindle  9766  fzfi  12082  rexanuz  13178  limsupgord  13295  limsupcl  13296  limsupgf  13298  limsupgle  13300  rlimres  13381  lo1res  13382  o1of2  13435  o1rlimmul  13441  ackbijnn  13640  bitsinv1  14092  bitsinvp1  14099  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  sadasslem  14120  sadeq  14122  smuval2  14132  smupval  14138  smueqlem  14140  prmrec  14440  isstruct2  14641  structcnvcnv  14643  ressbasss  14689  ressress  14694  restsspw  14829  pwsle  14889  submre  15002  isacs2  15050  isacs1i  15054  sscres  15192  rescabs  15202  resscat  15221  funcres2c  15270  coffth  15305  rescfth  15306  ressffth  15307  catccatid  15429  catcisolem  15433  catciso  15434  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476  yoniso  15554  isdrs2  15568  isacs3lem  15796  acsinfd  15810  acsdomd  15811  psssdm2  15845  tsrss  15853  idrespermg  16436  mvdco  16470  sylow2a  16639  lsmmod  16693  frgpnabllem2  16878  subrgpropd  17463  lssacs  17613  sralmod  17833  asplss  17978  ressmplbas  18118  subrgmpl  18122  opsrtoslem2  18149  mplind  18167  ressply1bas  18270  pf1rcl  18385  zringlpirlem2  18510  zringlpirlem3  18511  zlpirlem2  18515  zlpirlem3  18516  ofco2  18953  basdif0  19454  eltg4i  19461  ntrss2  19558  ntrin  19562  isopn3  19567  mreclatdemoBAD  19597  neiptoptop  19632  restbas  19659  resttopon  19662  restuni2  19668  restcld  19673  restfpw  19680  neitr  19681  ordtrest  19703  subbascn  19755  cnrest2r  19788  cnpresti  19789  cnprest  19790  lmss  19799  cnrmi  19861  restcnrm  19863  resthauslem  19864  fincmp  19893  imacmp  19897  fiuncmp  19904  cmpfi  19908  bwth  19910  cnconn  19923  iuncon  19929  clscon  19931  concompclo  19936  1stcrest  19954  subislly  19982  islly2  19985  cldllycmp  19996  hauspwdom  20002  kgeni  20038  llycmpkgen2  20051  1stckgenlem  20054  ptbasfi  20082  txcls  20105  ptclsg  20116  txcnp  20121  ptcnplem  20122  txtube  20141  txcmplem1  20142  txcmplem2  20143  txkgen  20153  xkopt  20156  xkococnlem  20160  txcon  20190  basqtop  20212  tgqtop  20213  kqdisj  20233  kqnrmlem1  20244  kqnrmlem2  20245  nrmhmph  20295  infil  20364  fbasrn  20385  trfg  20392  uzrest  20398  isufil2  20409  fmfnfmlem4  20458  hauspwpwf1  20488  txflf  20507  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem2  20553  tmdgsum2  20595  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  ustexsym  20718  ustund  20724  trust  20732  utoptop  20737  restutop  20740  blres  20934  met2ndci  21025  metrest  21027  restmetu  21090  tgioo  21301  zdis  21321  reconnlem2  21332  reconn  21333  cnheibor  21455  lebnum  21464  nmoleub2lem3  21598  nmoleub3  21602  cphsqrtcl  21631  tchcph  21680  cfilresi  21734  cfilres  21735  caussi  21736  causs  21737  minveclem4b  21846  minveclem4  21847  ovolfcl  21878  ovolfioo  21879  ovolficc  21880  ovolficcss  21881  ovolfsval  21882  ovolfsf  21883  ovollb  21890  ovoliunlem1  21913  ovolicc2lem1  21928  ovolicc2lem2  21929  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2lem5  21932  ovolicc2  21933  nulmbl  21946  voliunlem1  21960  ioombl1lem4  21971  ovolfs2  21980  uniiccdif  21987  uniioovol  21988  uniiccvol  21989  uniioombllem2a  21991  uniioombllem2  21992  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  uniioombllem6  21997  uniioombl  21998  dyadmbllem  22008  dyadmbl  22009  opnmbllem  22010  volcn  22015  volivth  22016  vitalilem2  22018  vitalilem4  22020  mbfadd  22068  mbfsub  22069  i1fima  22085  i1fima2  22086  i1fd  22088  i1fadd  22102  i1fmul  22103  itg1addlem2  22104  itg1addlem4  22106  itg1addlem5  22107  i1fres  22112  mbfmul  22133  itg2cnlem2  22169  bddmulibl  22245  ellimc2  22281  ellimc3  22283  limcflf  22285  limcresi  22289  limciun  22298  dvreslem  22313  dvres2lem  22314  dvres3a  22318  cpnres  22340  dvaddbr  22341  dvmulbr  22342  dvmptres3  22359  lhop1lem  22414  ig1peu  22572  taylfvallem1  22752  tayl0  22757  rlimcnp2  23296  xrlimcnp  23298  ppisval  23377  chtf  23382  efchtcl  23385  chtge0  23386  ppinprm  23426  chtprm  23427  chtnprm  23428  chtwordi  23430  chtdif  23432  efchtdvds  23433  chtlepsi  23481  chtleppi  23485  pclogsum  23490  chpval2  23493  chpchtsum  23494  chpub  23495  2sqlem8  23647  2sqlem9  23648  chebbnd1lem1  23654  chtppilimlem1  23658  rplogsumlem2  23670  rpvmasumlem  23672  rplogsum  23712  dirith2  23713  axtgsegcon  23861  axtg5seg  23862  axtgbtwnid  23863  axtgpasch  23864  axtgcont1  23865  tglng  23933  perpneq  24091  ragperp  24094  issubgo  25305  opidonOLD  25324  chdmm1i  26395  chm0i  26408  ledii  26454  lejdii  26456  pjoml2i  26503  pjoml4i  26505  cmcmlem  26509  cmbr4i  26519  osumcori  26561  pjssmii  26599  mayete3i  26646  mayete3iOLD  26647  riesz4  26983  riesz1  26984  cnlnadjeu  26997  nmopadjlei  27007  pjclem1  27114  pjci  27119  mdbr3  27216  mdbr4  27217  dmdbr2  27222  dmdbr5  27227  ssmd2  27231  mdslj1i  27238  mdslj2i  27239  mdsl1i  27240  mdsl2bi  27242  mdslmd1lem1  27244  mdslmd1lem2  27245  mdslmd2i  27249  csmdsymi  27253  cvexchlem  27287  atomli  27301  atcvat4i  27316  inindif  27414  disjxpin  27447  imadifxp  27458  suppss2f  27477  off2  27481  partfun  27516  resspos  27647  resstos  27648  submomnd  27700  suborng  27805  prsdm  27896  prsrn  27897  ordtrestNEW  27903  pnfneige0  27933  lmxrge0  27934  qqhnm  27971  qqhcn  27972  rrhre  27999  indf1ofs  28039  gsumesum  28067  esumlub  28068  esumcst  28071  esumpcvgval  28084  hasheuni  28091  esumcvg  28092  sigainb  28136  sibfinima  28281  sibfof  28282  eulerpartlemelr  28296  eulerpartlemgh  28317  eulerpartlemgf  28318  eulerpartlemgs2  28319  eulerpartlemn  28320  probmeasb  28369  cndprob01  28374  conpcon  28680  iccllyscon  28695  cvmsss2  28719  cvmcov2  28720  cvmopnlem  28723  cvmliftmolem2  28727  cvmlift2lem12  28759  mvrsfpw  28866  elmsta  28908  msubvrs  28920  mclsind  28930  nepss  29095  elrn3  29192  dfon2lem4  29218  wfrlem4  29346  frrlem4  29390  heicant  30049  opnmbllem0  30050  mblfinlem4  30054  mbfposadd  30062  trer  30134  neiin  30150  neibastop1  30177  neibastop2lem  30178  topmeet  30182  filnetlem3  30198  heibor1lem  30305  heiborlem1  30307  heiborlem3  30309  heiborlem10  30316  elrfi  30626  elrfirn  30627  fnwe2lem2  30997  aomclem2  31001  lsmfgcl  31020  lmhmfgima  31030  lmhmfgsplit  31032  lmhmlnmsplit  31033  hbt  31079  acsfn1p  31148  islptre  31625  sumnnodd  31636  limcresiooub  31648  limcresioolb  31649  limcleqr  31650  limclner  31657  limclr  31661  icccncfext  31690  fourierdlem20  31909  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem76  31965  fourierdlem103  31992  fourierdlem104  31993  fourierdlem113  32002  fouriersw  32014  lidlssbas  32728  rnghmresfn  32771  rnghmsscmap  32782  rngchomrnghmresOLD  32804  rhmresfn  32817  rhmsscmap  32828  rhmsubclem4  32897  onfrALTlem3  33316  onfrALTlem2  33318  onfrALTlem3VD  33687  onfrALTlem2VD  33689  iunconlem2  33735  bnj1293  33875  bj-ablsscmn  34656  lshpinN  34714  lcvexchlem1  34759  lcvexchlem5  34763  pmod1i  35572  pmodN  35574  osumcllem7N  35686  pexmidlem4N  35697  dochdmj1  37117  dochexmidlem4  37190  lcfrlem25  37294  mapd1o  37375  mapdin  37389  fiinfi  37758  xptrrel  37775  trrelind  37778  xphe  37804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489