Theorem inss1 3717

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
inss1

Proof of Theorem inss1

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3686	. . 3
2	1	simplbi 460	. 2
3	2	ssriv 3507	1

Syntax hints:  e.wcel 1818  i^icin 3474  C_wss 3475

This theorem is referenced by:  inss2  3718  ssinss1  3725  unabs  3727  nssinpss  3729  dfin4  3737  inv1  3812  disjdif  3900  uniintsn  4324  wefrc  4878  ordtri3or  4915  onfr  4922  ordelinel  4981  relin1  5125  resss  5302  resmpt3  5329  cnvcnvss  5466  funin  5660  funimass2  5667  fnresin1  5700  fnres  5702  fresin  5759  fresaun  5761  fresaunres2  5762  nfvres  5901  ssimaex  5938  fneqeql2  5996  funiunfv  6160  isoini2  6235  ofrfval  6548  ofval  6549  ofrval  6550  off  6554  ofres  6555  ofco  6560  fparlem3  6902  fparlem4  6903  smores  7042  smores2  7044  tfrlem5  7068  pmresg  7466  sbthlem7  7653  sbthcl  7659  infi  7763  imafi  7833  ixpfi2  7838  unifpw  7843  f1opwfi  7844  fival  7892  fi0  7900  dffi2  7903  elfiun  7910  dffi3  7911  marypha1lem  7913  ordtypelem3  7966  ordtypelem4  7967  ordtypelem6  7969  ordtypelem7  7970  ordtypelem8  7971  wdomima2g  8033  epfrs  8183  tskwe  8352  r0weon  8411  fodomfi2  8462  infpwfien  8464  ackbij1lem6  8626  ackbij1lem9  8629  ackbij1lem10  8630  ackbij1lem11  8631  ackbij1lem15  8635  ackbij1lem16  8636  fin23lem24  8723  fin23lem26  8726  fin23lem23  8727  fin23lem22  8728  fin23lem19  8737  isfin1-3  8787  ttukeylem6  8915  brdom3  8927  brdom5  8928  brdom4  8929  imadomg  8933  fpwwe2lem12  9040  canthp1lem2  9052  wunin  9112  tskin  9158  gruima  9201  ingru  9214  gruina  9217  grur1a  9218  nqerf  9329  nqerrel  9331  dedekindle  9766  hashun3  12452  hashdif  12476  rexanuz  13178  limsupgle  13300  rlimres  13381  lo1res  13382  lo1resb  13387  rlimresb  13388  o1resb  13389  lo1eq  13391  rlimeq  13392  o1of2  13435  o1rlimmul  13441  isercolllem2  13488  isercolllem3  13489  isercoll  13490  ackbijnn  13640  incexclem  13648  incexc  13649  bitsinvp1  14099  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  sadasslem  14120  sadeq  14122  bitsres  14123  smuval2  14132  smupval  14138  smueqlem  14140  smumul  14143  prmreclem2  14435  ramub2  14532  ramub1lem2  14545  fvsetsid  14657  ressinbas  14693  ressress  14694  submre  15002  submrc  15025  isacs2  15050  isacs1i  15054  mreacs  15055  acsfn  15056  invss  15155  sscres  15192  coffth  15305  catcisolem  15433  catciso  15434  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476  isdrs2  15568  isacs3lem  15796  isacs5lem  15799  acsfiindd  15807  psss  15844  psssdm2  15845  tsrss  15853  tsrdir  15868  resscntz  16369  sylow2a  16639  lsmmod  16693  frgpnabllem2  16878  gsumzres  16914  gsumzresOLD  16918  gsumzaddlem  16934  gsumzaddlemOLD  16936  dprddisj2  17087  dprddisj2OLD  17088  ablfac1eu  17124  ablfac2  17140  isunit  17306  lspextmo  17702  2idlval  17881  aspsubrg  17980  psrbagsn  18160  mplind  18167  zringlpirlem2  18510  zlpirlem2  18515  pjfval  18737  pjpm  18739  ofco2  18953  basdif0  19454  tgval2  19457  eltg3  19463  unitgOLD  19469  tgcl  19471  tgdom  19480  tgidm  19482  ppttop  19508  epttop  19510  ntropn  19550  ntrin  19562  mretopd  19593  mreclatdemoBAD  19597  neiptoptop  19632  restbas  19659  restfpw  19680  neitr  19681  restcls  19682  ordtrest  19703  subbascn  19755  cncls  19775  cnpresti  19789  cnprest  19790  fincmp  19893  cmpsublem  19899  cmpsub  19900  fiuncmp  19904  indiscon  19919  connsub  19922  cnconn  19923  iunconlem  19928  clscon  19931  concompclo  19936  islly2  19985  cldllycmp  19996  kgentopon  20039  llycmpkgen2  20051  1stckgenlem  20054  ptbasfi  20082  txcls  20105  txcnp  20121  ptcnplem  20122  txcnmpt  20125  txcmplem2  20143  hausdiag  20146  txkgen  20153  xkopt  20156  xkococnlem  20160  txcon  20190  qtoptop2  20200  basqtop  20212  tgqtop  20213  kqnrmlem1  20244  kqnrmlem2  20245  nrmhmph  20295  fbssfi  20338  filin  20355  infil  20364  fbasrn  20385  fgtr  20391  ufprim  20410  flimrest  20484  hauspwpwf1  20488  txflf  20507  fclsrest  20525  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem5  20556  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  ustund  20724  trust  20732  utoptop  20737  restutop  20740  cfiluweak  20798  xmetres  20867  metres  20868  blin2  20932  blbas  20933  blres  20934  setsmstopn  20981  met2ndci  21025  metrest  21027  ressxms  21028  tgioo  21301  xrsmopn  21317  zdis  21321  reconnlem1  21331  reconnlem2  21332  xrge0tsms  21339  cnheibor  21455  lebnum  21464  nmoleub2lem  21597  nmoleub2lem3  21598  nmoleub2lem2  21599  nmoleub3  21602  nmhmcn  21603  tchcph  21680  cfilresi  21734  cfilres  21735  caussi  21736  causs  21737  relcmpcmet  21755  minveclem4a  21845  minveclem4  21847  ismbl2  21938  cmmbl  21945  nulmbl2  21947  unmbl  21948  shftmbl  21949  volinun  21956  voliunlem1  21960  voliunlem2  21961  ioombl1lem4  21971  ioombl1  21972  ioorcl  21986  uniioombllem2  21992  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  uniioombl  21998  volivth  22016  vitalilem3  22019  vitalilem4  22020  vitalilem5  22021  vitali  22022  mbfadd  22068  mbfsub  22069  i1fima2  22086  i1fd  22088  i1fadd  22102  itg1addlem2  22104  itg1addlem4  22106  itg1addlem5  22107  itg1climres  22121  mbfmul  22133  itg2splitlem  22155  itg2split  22156  limcresi  22289  limciun  22298  limcun  22299  dvreslem  22313  dvres2lem  22314  dvres  22315  dvres3a  22318  dvaddbr  22341  dvmulbr  22342  dvfsumle  22422  dvfsumabs  22424  ig1peu  22572  taylfvallem1  22752  tayl0  22757  pilem2  22847  pilem3  22848  rlimcnp2  23296  xrlimcnp  23298  ppisval  23377  ppifi  23379  ppiprm  23425  ppinprm  23426  chtprm  23427  chtnprm  23428  chtdif  23432  efchtdvds  23433  ppidif  23437  ppiltx  23451  prmorcht  23452  ppiub  23479  chtlepsi  23481  chtleppi  23485  pclogsum  23490  vmasum  23491  chpval2  23493  chpchtsum  23494  chpub  23495  2sqlem8  23647  chebbnd1lem1  23654  chtppilimlem1  23658  rplogsumlem2  23670  rpvmasum2  23697  dchrisum0re  23698  rplogsum  23712  dirith2  23713  axtgcgrrflx  23859  axtgcgrid  23860  axtgsegcon  23861  axtg5seg  23862  axtgbtwnid  23863  axtgpasch  23864  axtgcont1  23865  perpcom  24090  perpneq  24091  ragperp  24094  opidonOLD  25324  flddivrng  25417  phnv  25729  minvecolem2  25791  minvecolem3  25792  minvecolem5  25797  minvecolem6  25798  minvecolem7  25799  hlimcaui  26154  chdmm1i  26395  chabs1  26434  chabs2  26435  ledii  26454  lejdii  26456  pjoml4i  26505  cmbr3i  26518  cmbr4i  26519  cmm1i  26524  osumcor2i  26562  3oalem4  26583  pjssmii  26599  pjocini  26616  pjini  26617  mayete3i  26646  mayete3iOLD  26647  riesz4  26983  riesz1  26984  cnlnadjeui  26996  cnlnadjeu  26997  cnlnssadj  26999  nmopadjlei  27007  pjin1i  27111  pjclem1  27114  stji1i  27161  stm1i  27162  dmdbr2  27222  ssmd1  27230  mdslj2i  27239  mdsl2bi  27242  mdslmd1lem1  27244  mdslmd2i  27249  atomli  27301  atcvat4i  27316  sumdmdlem2  27338  dmdbr5ati  27341  dmdbr6ati  27342  dmdbr7ati  27343  disjin  27446  disjxpin  27447  imadifxp  27458  off2  27481  ffsrn  27552  xrge0tsmsd  27775  ordtrestNEW  27903  qqhnm  27971  qqhcn  27972  rrhre  27999  indf1ofs  28039  esumval  28057  esumel  28058  gsumesum  28067  esumlub  28068  esumcst  28071  esumfsup  28076  esumpcvgval  28084  esumcvg  28092  sigainb  28136  measinb2  28194  sibfinima  28281  sibfof  28282  eulerpartlemelr  28296  eulerpartlem1  28306  eulerpartgbij  28311  eulerpartlemgvv  28315  eulerpartlemgu  28316  eulerpartlemgs2  28319  sseqf  28331  ballotlemfelz  28429  ballotlemfp1  28430  conpcon  28680  iccllyscon  28695  cvmsss2  28719  cvmcov2  28720  cvmopnlem  28723  cvmliftmolem2  28727  cvmliftlem15  28743  cvmlift2lem12  28759  mvrsfpw  28866  msrf  28902  elmsta  28908  mthmpps  28942  nepss  29095  dfon2lem4  29218  predss  29251  wfrlem4  29346  frrlem4  29390  nofulllem5  29466  txpss3v  29528  fixssdm  29556  fixssrn  29557  limitssson  29561  ontopbas  29893  ptrest  30048  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  mbfposadd  30062  fneer  30171  neibastop1  30177  neibastop2lem  30178  filnetlem3  30198  sstotbnd2  30270  ssbnd  30284  heibor1lem  30305  heiborlem1  30307  heiborlem3  30309  heiborlem5  30311  heiborlem6  30312  heiborlem10  30316  heibor  30317  exidcl  30338  elrfi  30626  elrfirn  30627  elrfirn2  30628  ismrcd1  30630  istopclsd  30632  isnacs2  30638  mrefg3  30640  isnacs3  30642  diophrw  30692  diophin  30706  aomclem2  31001  islmodfg  31015  lsmfgcl  31020  lmhmfgima  31030  lmhmfgsplit  31032  lmhmlnmsplit  31033  pwfi2f1o  31044  hbt  31079  acsfn1p  31148  islptre  31625  sumnnodd  31636  limclner  31657  cncfuni  31689  fouriersw  32014  rngcbas  32773  rngchomfval  32774  rngccofval  32778  dfrngc2  32780  rnghmsscmap2  32781  rnghmsscmap  32782  rngcsect  32788  funcrngcsetc  32806  ringcbas  32819  ringchomfval  32820  ringccofval  32824  dfringc2  32826  rhmsscmap2  32827  rhmsscmap  32828  rhmsscrnghm  32834  ringcsect  32839  funcringcsetc  32843  funcringcsetcOLD2lem9  32852  fldc  32891  fldhmsubc  32892  rngcrescrhm  32893  rhmsubclem1  32894  fldcOLD  32910  fldhmsubcOLD  32911  rngcrescrhmOLD  32912  rhmsubcOLDlem1  32913  onfrALTlem2  33318  onfrALTlem2VD  33689  bnj1292  33874  bj-ablssgrp  34654  lshpinN  34714  lcvexchlem5  34763  pmodlem2  35571  pmod1i  35572  pmodN  35574  osumcllem7N  35686  pexmidlem4N  35697  pl42lem3N  35705  djaclN  36863  dihoml4c  37103  dochdmj1  37117  djhcl  37127  dochexmidlem4  37190  mapd1o  37375  mapdin  37389  taupilemrplb  37695  taupilem2  37697  taupi  37698  fiinfi  37758  xptrrel  37775  trrelind  37778  rp-imass  37795

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