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

Theorem inss1 3606
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 3576 . . 3
21simplbi 448 . 2
32ssriv 3397 1
Colors of variables: wff set class
Syntax hints:  e.wcel 1732  i^icin 3364  C_wss 3365
This theorem is referenced by:  inss2  3607  ssinss1  3614  unabs  3616  nssinpss  3618  dfin4  3626  inv1  3699  disjdif  3786  uniintsn  4191  wefrc  4735  ordtri3or  4772  onfr  4779  ordelinel  4839  relin1  4979  resss  5157  resmpt3  5180  cnvcnvss  5312  funin  5503  funimass2  5510  fnresin1  5543  fnres  5545  fresin  5597  fresaun  5599  fresaunres2  5600  nfvres  5736  ssimaex  5772  fneqeql2  5828  funiunfv  5979  isoini2  6040  ofrfval  6338  ofval  6339  ofrval  6340  off  6344  ofres  6345  ofco  6350  fparlem3  6680  fparlem4  6681  smores  6776  smores2  6778  pmresg  7204  sbthlem7  7388  sbthcl  7394  infi  7497  imafi  7565  ixpfi2  7571  unifpw  7576  f1opwfi  7577  fival  7584  fi0  7592  dffi2  7595  elfiun  7602  dffi3  7603  marypha1lem  7605  ordtypelem3  7656  ordtypelem4  7657  ordtypelem6  7659  ordtypelem7  7660  ordtypelem8  7661  wdomima2g  7721  epfrs  7834  tskwe  8006  r0weon  8065  fodomfi2  8112  infpwfien  8114  ackbij1lem6  8276  ackbij1lem9  8279  ackbij1lem10  8280  ackbij1lem11  8281  ackbij1lem15  8285  ackbij1lem16  8286  fin23lem24  8373  fin23lem26  8376  fin23lem23  8377  fin23lem22  8378  fin23lem19  8387  isfin1-3  8437  ttukeylem6  8565  brdom3  8577  brdom5  8578  brdom4  8579  imadomg  8583  fpwwe2lem12  8687  canthp1lem2  8699  wunin  8759  tskin  8805  gruima  8848  ingru  8861  gruina  8864  grur1a  8865  nqerf  8978  nqerrel  8980  hashun3  11996  hashdif  12017  rexanuz  12680  limsupgle  12802  rlimres  12883  lo1res  12884  lo1resb  12889  rlimresb  12890  o1resb  12891  lo1eq  12893  rlimeq  12894  o1of2  12937  o1rlimmul  12943  isercolllem2  12990  isercolllem3  12991  isercoll  12992  ackbijnn  13138  incexclem  13146  incexc  13147  bitsinvp1  13492  sadcaddlem  13500  sadadd2lem  13502  sadadd3  13504  sadaddlem  13509  sadasslem  13513  sadeq  13515  bitsres  13516  smuval2  13525  smupval  13531  smueqlem  13533  smumul  13536  prmreclem2  13825  ramub2  13922  ramub1lem2  13935  fvsetsid  14046  ressinbas  14079  ressress  14080  submre  14384  submrc  14407  isacs2  14432  isacs1i  14436  mreacs  14437  acsfn  14438  invss  14540  sscres  14577  coffth  14687  catcisolem  14815  catciso  14816  catcoppccl  14817  catcfuccl  14818  catcxpccl  14858  isdrs2  14950  isacs3lem  15177  isacs5lem  15180  acsfiindd  15188  psss  15225  psssdm2  15226  tsrss  15234  tsrdir  15249  resscntz  15739  sylow2a  15862  lsmmod  15916  frgpnabllem2  16095  gsumzres  16127  gsumzaddlem  16136  dprddisj2  16212  ablfac1eu  16246  ablfac2  16262  isunit  16378  lspextmo  16751  2idlval  16929  aspsubrg  17015  psrbagsn  17180  mplind  17187  zlpirlem2  17394  pjfval  17558  pjpm  17560  frlmsplit2  17723  ofco2  17802  basdif0  18032  tgval2  18035  eltg3  18041  unitg  18046  tgcl  18048  tgdom  18057  tgidm  18059  ppttop  18085  epttop  18087  ntropn  18127  ntrin  18139  mretopd  18170  mreclatdemoBAD  18174  neiptoptop  18209  restbas  18236  restfpw  18257  neitr  18258  restcls  18259  ordtrest  18280  subbascn  18332  cncls  18352  cnpresti  18366  cnprest  18367  fincmp  18470  cmpsublem  18476  cmpsub  18477  fiuncmp  18481  indiscon  18496  connsub  18499  cnconn  18500  iunconlem  18505  clscon  18508  concompclo  18513  islly2  18562  cldllycmp  18573  kgentopon  18585  llycmpkgen2  18597  1stckgenlem  18600  ptbasfi  18628  txcls  18651  txcnp  18667  ptcnplem  18668  txcnmpt  18671  txcmplem2  18689  hausdiag  18692  txkgen  18699  xkopt  18702  xkococnlem  18706  txcon  18736  qtoptop2  18746  basqtop  18758  tgqtop  18759  kqnrmlem1  18790  kqnrmlem2  18791  nrmhmph  18841  fbssfi  18884  filin  18901  infil  18910  fbasrn  18931  fgtr  18937  ufprim  18956  flimrest  19030  hauspwpwf1  19034  txflf  19053  fclsrest  19071  alexsubALTlem3  19095  alexsubALTlem4  19096  ptcmplem5  19102  tsmsres  19188  tsmsxplem1  19197  ustund  19266  trust  19274  utoptop  19279  restutop  19282  cfiluweak  19340  xmetres  19409  metres  19410  blin2  19474  blbas  19475  blres  19476  setsmstopn  19523  met2ndci  19567  metrest  19569  ressxms  19570  tgioo  19842  xrsmopn  19858  zdis  19862  reconnlem1  19872  reconnlem2  19873  xrge0tsms  19880  cnheibor  19995  lebnum  20004  nmoleub2lem  20137  nmoleub2lem3  20138  nmoleub2lem2  20139  nmoleub3  20142  nmhmcn  20143  tchcph  20209  cfilresi  20263  cfilres  20264  caussi  20265  causs  20266  relcmpcmet  20284  minveclem4a  20346  minveclem4  20348  ismbl2  20438  cmmbl  20444  nulmbl2  20446  unmbl  20447  shftmbl  20448  volinun  20455  voliunlem1  20459  voliunlem2  20460  ioombl1lem4  20470  ioombl1  20471  ioorcl  20484  uniioombllem2  20490  uniioombllem3  20492  uniioombllem4  20493  uniioombllem5  20494  uniioombl  20496  volivth  20514  vitalilem3  20517  vitalilem4  20518  vitalilem5  20519  vitali  20520  mbfadd  20566  mbfsub  20567  i1fima2  20584  i1fd  20586  i1fadd  20600  itg1addlem2  20602  itg1addlem4  20604  itg1addlem5  20605  itg1climres  20619  mbfmul  20631  itg2splitlem  20653  itg2split  20654  limcresi  20787  limciun  20796  limcun  20797  dvreslem  20811  dvres2lem  20812  dvres  20813  dvres3a  20816  dvaddbr  20839  dvmulbr  20840  dvfsumle  20920  dvfsumabs  20922  ig1peu  21109  taylfvallem1  21288  tayl0  21293  pilem2  21383  pilem3  21384  rlimcnp2  21826  xrlimcnp  21828  ppisval  21907  ppifi  21909  ppiprm  21955  ppinprm  21956  chtprm  21957  chtnprm  21958  chtdif  21962  efchtdvds  21963  ppidif  21967  ppiltx  21981  prmorcht  21982  ppiub  22009  chtlepsi  22011  chtleppi  22015  pclogsum  22020  vmasum  22021  chpval2  22023  chpchtsum  22024  chpub  22025  2sqlem8  22177  chebbnd1lem1  22184  chtppilimlem1  22188  rplogsumlem2  22200  rpvmasum2  22227  dchrisum0re  22228  rplogsum  22242  dirith2  22243  opidon  22931  flddivrng  23024  phnv  23336  minvecolem2  23398  minvecolem3  23399  minvecolem5  23404  minvecolem6  23405  minvecolem7  23406  hlimcaui  23761  chdmm1i  24002  chabs1  24041  chabs2  24042  ledii  24061  lejdii  24063  pjoml4i  24112  cmbr3i  24125  cmbr4i  24126  cmm1i  24131  osumcor2i  24169  3oalem4  24190  pjssmii  24206  pjocini  24223  pjini  24224  mayete3i  24253  mayete3iOLD  24254  riesz4  24590  riesz1  24591  cnlnadjeui  24603  cnlnadjeu  24604  cnlnssadj  24606  nmopadjlei  24614  pjin1i  24718  pjclem1  24721  stji1i  24768  stm1i  24769  dmdbr2  24829  ssmd1  24837  mdslj2i  24846  mdsl2bi  24849  mdslmd1lem1  24851  mdslmd2i  24856  atomli  24908  atcvat4i  24923  sumdmdlem2  24945  dmdbr5ati  24948  dmdbr6ati  24949  dmdbr7ati  24950  disjin  25057  disjxpin  25058  imadifxp  25067  off2  25089  ffsrn  25159  gsumle  25406  xrge0tsmsd  25414  ordtrestNEW  25530  qqhnm  25599  qqhcn  25600  rrhre  25627  indf1ofs  25662  esumval  25680  esumel  25681  gsumesum  25690  esumlub  25691  esumcst  25694  esumfsup  25699  esumpcvgval  25707  esumcvg  25715  sigainb  25759  measunl  25810  measinb2  25817  sibfinima  25899  sibfof  25900  eulerpartlemelr  25914  eulerpartlem1  25924  eulerpartgbij  25929  eulerpartlemgvv  25933  eulerpartlemgu  25934  eulerpartlemgs2  25937  ballotlemfelz  26023  ballotlemfp1  26024  conpcon  26270  iccllyscon  26285  cvmsss2  26309  cvmcov2  26310  cvmopnlem  26313  cvmliftmolem2  26317  cvmliftlem15  26333  cvmlift2lem12  26349  nepss  26514  dedekindle  26527  dfon2lem4  26752  predss  26785  wfrlem4  26880  frrlem4  26924  nofulllem5  27000  txpss3v  27062  fixssdm  27090  fixssrn  27091  limitssson  27095  ontopbas  27517  mblfinlem3  27610  mblfinlem4  27611  ismblfin  27612  mbfposadd  27619  fneer  27740  fnessref  27745  neibastop1  27760  neibastop2lem  27761  filnetlem3  27781  sstotbnd2  27855  ssbnd  27869  heibor1lem  27890  heiborlem1  27892  heiborlem3  27894  heiborlem5  27896  heiborlem6  27897  heiborlem10  27901  heibor  27902  exidcl  27923  elrfi  28178  elrfirn  28179  elrfirn2  28180  ismrcd1  28182  istopclsd  28184  isnacs2  28190  mrefg3  28192  isnacs3  28194  diophrw  28245  diophin  28259  aomclem2  28556  islmodfg  28570  lsmfgcl  28575  lmhmfgima  28585  lmhmfgsplit  28587  lmhmlnmsplit  28588  pwfi2f1o  28600  hbt  28674  acsfn1p  28738  onfrALTlem2  30100  onfrALTlem2VD  30471  bnj1292  30657  lshpinN  31337  lcvexchlem5  31386  pmodlem2  32194  pmod1i  32195  pmodN  32197  osumcllem7N  32309  pexmidlem4N  32320  pl42lem3N  32328  djaclN  33484  dihoml4c  33724  dochdmj1  33738  djhcl  33748  dochexmidlem4  33811  mapd1o  33996  mapdin  34010  taupilemrplb  34317  taupilem2  34319  taupi  34320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-v 3017  df-in 3372  df-ss 3379
  Copyright terms: Public domain W3C validator