MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inss1 Unicode version

Theorem inss1 3570
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.
StepHypRef Expression
1 elin 3539 . . 3
21simplbi 460 . 2
32ssriv 3360 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1756  i^icin 3327  C_wss 3328
This theorem is referenced by:  inss2  3571  ssinss1  3578  unabs  3580  nssinpss  3582  dfin4  3590  inv1  3664  disjdif  3751  uniintsn  4165  wefrc  4714  ordtri3or  4751  onfr  4758  ordelinel  4817  relin1  4957  resss  5134  resmpt3  5157  cnvcnvss  5292  funin  5485  funimass2  5492  fnresin1  5525  fnres  5527  fresin  5580  fresaun  5582  fresaunres2  5583  nfvres  5720  ssimaex  5756  fneqeql2  5812  funiunfv  5965  isoini2  6030  ofrfval  6328  ofval  6329  ofrval  6330  off  6334  ofres  6335  ofco  6340  fparlem3  6674  fparlem4  6675  smores  6813  smores2  6815  tfrlem5  6839  pmresg  7240  sbthlem7  7427  sbthcl  7433  infi  7536  imafi  7604  ixpfi2  7609  unifpw  7614  f1opwfi  7615  fival  7662  fi0  7670  dffi2  7673  elfiun  7680  dffi3  7681  marypha1lem  7683  ordtypelem3  7734  ordtypelem4  7735  ordtypelem6  7737  ordtypelem7  7738  ordtypelem8  7739  wdomima2g  7801  epfrs  7951  tskwe  8120  r0weon  8179  fodomfi2  8230  infpwfien  8232  ackbij1lem6  8394  ackbij1lem9  8397  ackbij1lem10  8398  ackbij1lem11  8399  ackbij1lem15  8403  ackbij1lem16  8404  fin23lem24  8491  fin23lem26  8494  fin23lem23  8495  fin23lem22  8496  fin23lem19  8505  isfin1-3  8555  ttukeylem6  8683  brdom3  8695  brdom5  8696  brdom4  8697  imadomg  8701  fpwwe2lem12  8808  canthp1lem2  8820  wunin  8880  tskin  8926  gruima  8969  ingru  8982  gruina  8985  grur1a  8986  nqerf  9099  nqerrel  9101  dedekindle  9534  hashun3  12147  hashdif  12168  rexanuz  12833  limsupgle  12955  rlimres  13036  lo1res  13037  lo1resb  13042  rlimresb  13043  o1resb  13044  lo1eq  13046  rlimeq  13047  o1of2  13090  o1rlimmul  13096  isercolllem2  13143  isercolllem3  13144  isercoll  13145  ackbijnn  13291  incexclem  13299  incexc  13300  bitsinvp1  13645  sadcaddlem  13653  sadadd2lem  13655  sadadd3  13657  sadaddlem  13662  sadasslem  13666  sadeq  13668  bitsres  13669  smuval2  13678  smupval  13684  smueqlem  13686  smumul  13689  prmreclem2  13978  ramub2  14075  ramub1lem2  14088  fvsetsid  14199  ressinbas  14234  ressress  14235  submre  14543  submrc  14566  isacs2  14591  isacs1i  14595  mreacs  14596  acsfn  14597  invss  14699  sscres  14736  coffth  14846  catcisolem  14974  catciso  14975  catcoppccl  14976  catcfuccl  14977  catcxpccl  15017  isdrs2  15109  isacs3lem  15336  isacs5lem  15339  acsfiindd  15347  psss  15384  psssdm2  15385  tsrss  15393  tsrdir  15408  resscntz  15849  sylow2a  16118  lsmmod  16172  frgpnabllem2  16352  gsumzres  16388  gsumzresOLD  16392  gsumzaddlem  16408  gsumzaddlemOLD  16410  dprddisj2  16537  dprddisj2OLD  16538  ablfac1eu  16574  ablfac2  16590  isunit  16749  lspextmo  17137  2idlval  17315  aspsubrg  17402  psrbagsn  17577  mplind  17584  zringlpirlem2  17904  zlpirlem2  17909  pjfval  18131  pjpm  18133  ofco2  18332  basdif0  18558  tgval2  18561  eltg3  18567  unitg  18572  tgcl  18574  tgdom  18583  tgidm  18585  ppttop  18611  epttop  18613  ntropn  18653  ntrin  18665  mretopd  18696  mreclatdemoBAD  18700  neiptoptop  18735  restbas  18762  restfpw  18783  neitr  18784  restcls  18785  ordtrest  18806  subbascn  18858  cncls  18878  cnpresti  18892  cnprest  18893  fincmp  18996  cmpsublem  19002  cmpsub  19003  fiuncmp  19007  indiscon  19022  connsub  19025  cnconn  19026  iunconlem  19031  clscon  19034  concompclo  19039  islly2  19088  cldllycmp  19099  kgentopon  19111  llycmpkgen2  19123  1stckgenlem  19126  ptbasfi  19154  txcls  19177  txcnp  19193  ptcnplem  19194  txcnmpt  19197  txcmplem2  19215  hausdiag  19218  txkgen  19225  xkopt  19228  xkococnlem  19232  txcon  19262  qtoptop2  19272  basqtop  19284  tgqtop  19285  kqnrmlem1  19316  kqnrmlem2  19317  nrmhmph  19367  fbssfi  19410  filin  19427  infil  19436  fbasrn  19457  fgtr  19463  ufprim  19482  flimrest  19556  hauspwpwf1  19560  txflf  19579  fclsrest  19597  alexsubALTlem3  19621  alexsubALTlem4  19622  ptcmplem5  19628  tsmsresOLD  19717  tsmsres  19718  tsmsxplem1  19727  ustund  19796  trust  19804  utoptop  19809  restutop  19812  cfiluweak  19870  xmetres  19939  metres  19940  blin2  20004  blbas  20005  blres  20006  setsmstopn  20053  met2ndci  20097  metrest  20099  ressxms  20100  tgioo  20373  xrsmopn  20389  zdis  20393  reconnlem1  20403  reconnlem2  20404  xrge0tsms  20411  cnheibor  20527  lebnum  20536  nmoleub2lem  20669  nmoleub2lem3  20670  nmoleub2lem2  20671  nmoleub3  20674  nmhmcn  20675  tchcph  20752  cfilresi  20806  cfilres  20807  caussi  20808  causs  20809  relcmpcmet  20827  minveclem4a  20917  minveclem4  20919  ismbl2  21010  cmmbl  21016  nulmbl2  21018  unmbl  21019  shftmbl  21020  volinun  21027  voliunlem1  21031  voliunlem2  21032  ioombl1lem4  21042  ioombl1  21043  ioorcl  21057  uniioombllem2  21063  uniioombllem3  21065  uniioombllem4  21066  uniioombllem5  21067  uniioombl  21069  volivth  21087  vitalilem3  21090  vitalilem4  21091  vitalilem5  21092  vitali  21093  mbfadd  21139  mbfsub  21140  i1fima2  21157  i1fd  21159  i1fadd  21173  itg1addlem2  21175  itg1addlem4  21177  itg1addlem5  21178  itg1climres  21192  mbfmul  21204  itg2splitlem  21226  itg2split  21227  limcresi  21360  limciun  21369  limcun  21370  dvreslem  21384  dvres2lem  21385  dvres  21386  dvres3a  21389  dvaddbr  21412  dvmulbr  21413  dvfsumle  21493  dvfsumabs  21495  ig1peu  21643  taylfvallem1  21822  tayl0  21827  pilem2  21917  pilem3  21918  rlimcnp2  22360  xrlimcnp  22362  ppisval  22441  ppifi  22443  ppiprm  22489  ppinprm  22490  chtprm  22491  chtnprm  22492  chtdif  22496  efchtdvds  22497  ppidif  22501  ppiltx  22515  prmorcht  22516  ppiub  22543  chtlepsi  22545  chtleppi  22549  pclogsum  22554  vmasum  22555  chpval2  22557  chpchtsum  22558  chpub  22559  2sqlem8  22711  chebbnd1lem1  22718  chtppilimlem1  22722  rplogsumlem2  22734  rpvmasum2  22761  dchrisum0re  22762  rplogsum  22776  dirith2  22777  axtgcgrrflx  22923  axtgcgrid  22924  axtgsegcon  22925  axtg5seg  22926  axtgbtwnid  22927  axtgpasch  22928  axtgcont1  22929  perpcom  23104  perpneq  23105  ragperp  23108  opidon  23809  flddivrng  23902  phnv  24214  minvecolem2  24276  minvecolem3  24277  minvecolem5  24282  minvecolem6  24283  minvecolem7  24284  hlimcaui  24639  chdmm1i  24880  chabs1  24919  chabs2  24920  ledii  24939  lejdii  24941  pjoml4i  24990  cmbr3i  25003  cmbr4i  25004  cmm1i  25009  osumcor2i  25047  3oalem4  25068  pjssmii  25084  pjocini  25101  pjini  25102  mayete3i  25131  mayete3iOLD  25132  riesz4  25468  riesz1  25469  cnlnadjeui  25481  cnlnadjeu  25482  cnlnssadj  25484  nmopadjlei  25492  pjin1i  25596  pjclem1  25599  stji1i  25646  stm1i  25647  dmdbr2  25707  ssmd1  25715  mdslj2i  25724  mdsl2bi  25727  mdslmd1lem1  25729  mdslmd2i  25734  atomli  25786  atcvat4i  25801  sumdmdlem2  25823  dmdbr5ati  25826  dmdbr6ati  25827  dmdbr7ati  25828  disjin  25929  disjxpin  25930  imadifxp  25939  off2  25959  ffsrn  26029  gsumle  26246  xrge0tsmsd  26253  ordtrestNEW  26351  qqhnm  26419  qqhcn  26420  rrhre  26447  indf1ofs  26482  esumval  26500  esumel  26501  gsumesum  26510  esumlub  26511  esumcst  26514  esumfsup  26519  esumpcvgval  26527  esumcvg  26535  sigainb  26579  measunl  26630  measinb2  26637  sibfinima  26725  sibfof  26726  eulerpartlemelr  26740  eulerpartlem1  26750  eulerpartgbij  26755  eulerpartlemgvv  26759  eulerpartlemgu  26760  eulerpartlemgs2  26763  sseqf  26775  ballotlemfelz  26873  ballotlemfp1  26874  conpcon  27124  iccllyscon  27139  cvmsss2  27163  cvmcov2  27164  cvmopnlem  27167  cvmliftmolem2  27171  cvmliftlem15  27187  cvmlift2lem12  27203  nepss  27374  dfon2lem4  27599  predss  27632  wfrlem4  27727  frrlem4  27771  nofulllem5  27847  txpss3v  27909  fixssdm  27937  fixssrn  27938  limitssson  27942  ontopbas  28274  ptrest  28425  mblfinlem3  28430  mblfinlem4  28431  ismblfin  28432  mbfposadd  28439  fneer  28560  fnessref  28565  neibastop1  28580  neibastop2lem  28581  filnetlem3  28601  sstotbnd2  28673  ssbnd  28687  heibor1lem  28708  heiborlem1  28710  heiborlem3  28712  heiborlem5  28714  heiborlem6  28715  heiborlem10  28719  heibor  28720  exidcl  28741  elrfi  29030  elrfirn  29031  elrfirn2  29032  ismrcd1  29034  istopclsd  29036  isnacs2  29042  mrefg3  29044  isnacs3  29046  diophrw  29097  diophin  29111  aomclem2  29408  islmodfg  29422  lsmfgcl  29427  lmhmfgima  29437  lmhmfgsplit  29439  lmhmlnmsplit  29440  pwfi2f1o  29451  hbt  29486  acsfn1p  29556  onfrALTlem2  31254  onfrALTlem2VD  31625  bnj1292  31809  bj-ablssgrp  32574  lshpinN  32634  lcvexchlem5  32683  pmodlem2  33491  pmod1i  33492  pmodN  33494  osumcllem7N  33606  pexmidlem4N  33617  pl42lem3N  33625  djaclN  34781  dihoml4c  35021  dochdmj1  35035  djhcl  35045  dochexmidlem4  35108  mapd1o  35293  mapdin  35307  taupilemrplb  35614  taupilem2  35616  taupi  35617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-in 3335  df-ss 3342
  Copyright terms: Public domain W3C validator