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

Theorem inss1 3659
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  |-  ( A  i^i  B )  C_  A

Proof of Theorem inss1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elin 3626 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
21simplbi 458 . 2  |-  ( x  e.  ( A  i^i  B )  ->  x  e.  A )
32ssriv 3446 1  |-  ( A  i^i  B )  C_  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842    i^i cin 3413    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-in 3421  df-ss 3428
This theorem is referenced by:  inss2  3660  ssinss1  3667  unabs  3680  nssinpss  3682  dfin4  3690  inv1  3766  disjdif  3844  uniintsn  4265  wefrc  4817  relin1  4940  resss  5117  resmpt3  5144  cnvcnvss  5278  predss  5374  ordtri3or  5442  onfr  5449  ordelinel  5508  funin  5636  funimass2  5643  fnresin1  5676  fnres  5678  fresin  5737  fresaun  5739  fresaunres2  5740  nfvres  5879  ssimaex  5914  fneqeql2  5974  funiunfv  6141  isoini2  6218  ofrfval  6529  ofval  6530  ofrval  6531  off  6536  ofres  6537  ofco  6542  fparlem3  6886  fparlem4  6887  wfrlem4  7024  smores  7056  smores2  7058  tfrlem5  7083  pmresg  7484  sbthlem7  7671  sbthcl  7677  infi  7778  imafi  7847  ixpfi2  7852  unifpw  7857  f1opwfi  7858  fival  7906  fi0  7914  dffi2  7917  elfiun  7924  dffi3  7925  marypha1lem  7927  ordtypelem3  7979  ordtypelem4  7980  ordtypelem6  7982  ordtypelem7  7983  ordtypelem8  7984  wdomima2g  8046  epfrs  8194  tskwe  8363  r0weon  8422  fodomfi2  8473  infpwfien  8475  ackbij1lem6  8637  ackbij1lem9  8640  ackbij1lem10  8641  ackbij1lem11  8642  ackbij1lem15  8646  ackbij1lem16  8647  fin23lem24  8734  fin23lem26  8737  fin23lem23  8738  fin23lem22  8739  fin23lem19  8748  isfin1-3  8798  ttukeylem6  8926  brdom3  8938  brdom5  8939  brdom4  8940  imadomg  8944  fpwwe2lem12  9049  canthp1lem2  9061  wunin  9121  tskin  9167  gruima  9210  ingru  9223  gruina  9226  grur1a  9227  nqerf  9338  nqerrel  9340  dedekindle  9779  hashun3  12500  hashdif  12525  xptrrel  12963  rexanuz  13327  limsupgle  13449  rlimres  13530  lo1res  13531  lo1resb  13536  rlimresb  13537  o1resb  13538  lo1eq  13540  rlimeq  13541  o1of2  13584  o1rlimmul  13590  isercolllem2  13637  isercolllem3  13638  isercoll  13639  ackbijnn  13791  incexclem  13799  incexc  13800  bitsinvp1  14308  sadcaddlem  14316  sadadd2lem  14318  sadadd3  14320  sadaddlem  14325  sadasslem  14329  sadeq  14331  bitsres  14332  smuval2  14341  smupval  14347  smueqlem  14349  smumul  14352  prmreclem2  14644  ramub2  14741  ramub1lem2  14754  fvsetsid  14868  ressinbas  14904  ressress  14906  submre  15219  submrc  15242  isacs2  15267  isacs1i  15271  mreacs  15272  acsfn  15273  invss  15374  sscres  15436  coffth  15549  catcisolem  15709  catciso  15710  catcoppccl  15711  catcfuccl  15712  catcxpccl  15800  isdrs2  15892  isacs3lem  16120  isacs5lem  16123  acsfiindd  16131  psss  16168  psssdm2  16169  tsrss  16177  tsrdir  16192  resscntz  16693  sylow2a  16963  lsmmod  17017  frgpnabllem2  17202  gsumzres  17238  gsumzresOLD  17242  gsumzaddlem  17258  gsumzaddlemOLD  17260  dprddisj2  17407  dprddisj2OLD  17408  ablfac1eu  17444  ablfac2  17460  isunit  17626  lspextmo  18022  2idlval  18201  aspsubrg  18300  psrbagsn  18480  mplind  18487  zringlpirlem2  18823  pjfval  19035  pjpm  19037  ofco2  19245  basdif0  19746  tgval2  19749  eltg3  19755  unitgOLD  19761  tgcl  19763  tgdom  19772  tgidm  19774  ppttop  19800  epttop  19802  ntropn  19842  ntrin  19854  mretopd  19886  mreclatdemoBAD  19890  neiptoptop  19925  restbas  19952  restfpw  19973  neitr  19974  restcls  19975  ordtrest  19996  subbascn  20048  cncls  20068  cnpresti  20082  cnprest  20083  fincmp  20186  cmpsublem  20192  cmpsub  20193  fiuncmp  20197  indiscon  20211  connsub  20214  cnconn  20215  iunconlem  20220  clscon  20223  concompclo  20228  islly2  20277  cldllycmp  20288  kgentopon  20331  llycmpkgen2  20343  1stckgenlem  20346  ptbasfi  20374  txcls  20397  txcnp  20413  ptcnplem  20414  txcnmpt  20417  txcmplem2  20435  hausdiag  20438  txkgen  20445  xkopt  20448  xkococnlem  20452  txcon  20482  qtoptop2  20492  basqtop  20504  tgqtop  20505  kqnrmlem1  20536  kqnrmlem2  20537  nrmhmph  20587  fbssfi  20630  filin  20647  infil  20656  fbasrn  20677  fgtr  20683  ufprim  20702  flimrest  20776  hauspwpwf1  20780  txflf  20799  fclsrest  20817  alexsubALTlem3  20841  alexsubALTlem4  20842  ptcmplem5  20848  tsmsresOLD  20937  tsmsres  20938  tsmsxplem1  20947  ustund  21016  trust  21024  utoptop  21029  restutop  21032  cfiluweak  21090  xmetres  21159  metres  21160  blin2  21224  blbas  21225  blres  21226  setsmstopn  21273  met2ndci  21317  metrest  21319  ressxms  21320  tgioo  21593  xrsmopn  21609  zdis  21613  reconnlem1  21623  reconnlem2  21624  xrge0tsms  21631  cnheibor  21747  lebnum  21756  nmoleub2lem  21889  nmoleub2lem3  21890  nmoleub2lem2  21891  nmoleub3  21894  nmhmcn  21895  tchcph  21972  cfilresi  22026  cfilres  22027  caussi  22028  causs  22029  relcmpcmet  22047  minveclem4a  22137  minveclem4  22139  ismbl2  22230  cmmbl  22237  nulmbl2  22239  unmbl  22240  shftmbl  22241  volinun  22248  voliunlem1  22252  voliunlem2  22253  ioombl1lem4  22263  ioombl1  22264  ioorcl  22278  uniioombllem2  22284  uniioombllem3  22286  uniioombllem4  22287  uniioombllem5  22288  uniioombl  22290  volivth  22308  vitalilem3  22311  vitalilem4  22312  vitalilem5  22313  vitali  22314  mbfadd  22360  mbfsub  22361  i1fima2  22378  i1fd  22380  i1fadd  22394  itg1addlem2  22396  itg1addlem4  22398  itg1addlem5  22399  itg1climres  22413  mbfmul  22425  itg2splitlem  22447  itg2split  22448  limcresi  22581  limciun  22590  limcun  22591  dvreslem  22605  dvres2lem  22606  dvres  22607  dvres3a  22610  dvaddbr  22633  dvmulbr  22634  dvfsumle  22714  dvfsumabs  22716  ig1peu  22864  taylfvallem1  23044  tayl0  23049  pilem2  23139  pilem3  23140  rlimcnp2  23622  xrlimcnp  23624  ppisval  23758  ppifi  23760  ppiprm  23806  ppinprm  23807  chtprm  23808  chtnprm  23809  chtdif  23813  efchtdvds  23814  ppidif  23818  ppiltx  23832  prmorcht  23833  ppiub  23860  chtlepsi  23862  chtleppi  23866  pclogsum  23871  vmasum  23872  chpval2  23874  chpchtsum  23875  chpub  23876  2sqlem8  24028  chebbnd1lem1  24035  chtppilimlem1  24039  rplogsumlem2  24051  rpvmasum2  24078  dchrisum0re  24079  rplogsum  24093  dirith2  24094  axtgcgrrflx  24238  axtgcgrid  24239  axtgsegcon  24240  axtg5seg  24241  axtgbtwnid  24242  axtgpasch  24243  axtgcont1  24244  perpcom  24476  perpneq  24477  ragperp  24480  opidonOLD  25738  flddivrng  25831  phnv  26143  minvecolem2  26205  minvecolem3  26206  minvecolem5  26211  minvecolem6  26212  minvecolem7  26213  hlimcaui  26568  chdmm1i  26809  chabs1  26848  chabs2  26849  ledii  26868  lejdii  26870  pjoml4i  26919  cmbr3i  26932  cmbr4i  26933  cmm1i  26938  osumcor2i  26976  3oalem4  26997  pjssmii  27013  pjocini  27030  pjini  27031  mayete3i  27060  riesz4  27396  riesz1  27397  cnlnadjeui  27409  cnlnadjeu  27410  cnlnssadj  27412  nmopadjlei  27420  pjin1i  27524  pjclem1  27527  stji1i  27574  stm1i  27575  dmdbr2  27635  ssmd1  27643  mdslj2i  27652  mdsl2bi  27655  mdslmd1lem1  27657  mdslmd2i  27662  atomli  27714  atcvat4i  27729  sumdmdlem2  27751  dmdbr5ati  27754  dmdbr6ati  27755  dmdbr7ati  27756  disjin  27878  disjxpin  27880  imadifxp  27894  off2  27924  ffsrn  27999  gsummptres  28227  xrge0tsmsd  28228  ordtrestNEW  28356  qqhnm  28423  qqhcn  28424  rrhre  28451  indf1ofs  28473  esumval  28493  esumel  28494  gsumesum  28506  esumlub  28507  esumcst  28510  esumfsup  28517  esumpcvgval  28525  esumcvg  28533  sigainb  28584  ldgenpisyslem1  28611  measinb2  28671  sibfinima  28787  sibfof  28788  eulerpartlemelr  28802  eulerpartlem1  28812  eulerpartgbij  28817  eulerpartlemgvv  28821  eulerpartlemgu  28822  eulerpartlemgs2  28825  sseqf  28837  ballotlemfelz  28935  ballotlemfp1  28936  bnj1292  29201  conpcon  29532  iccllyscon  29547  cvmsss2  29571  cvmcov2  29572  cvmopnlem  29575  cvmliftmolem2  29579  cvmliftlem15  29595  cvmlift2lem12  29611  mvrsfpw  29718  msrf  29754  elmsta  29760  mthmpps  29794  nepss  29924  dfon2lem4  30005  frrlem4  30090  nofulllem5  30166  txpss3v  30216  fixssdm  30244  fixssrn  30245  limitssson  30249  fneer  30581  neibastop1  30587  neibastop2lem  30588  filnetlem3  30608  ontopbas  30660  bj-ablssgrp  31218  taupilemrplb  31246  taupilem2  31248  taupi  31249  ptrest  31420  mblfinlem3  31425  mblfinlem4  31426  ismblfin  31427  mbfposadd  31434  sstotbnd2  31552  ssbnd  31566  heibor1lem  31587  heiborlem1  31589  heiborlem3  31591  heiborlem5  31593  heiborlem6  31594  heiborlem10  31598  heibor  31599  exidcl  31620  lshpinN  32007  lcvexchlem5  32056  pmodlem2  32864  pmod1i  32865  pmodN  32867  osumcllem7N  32979  pexmidlem4N  32990  pl42lem3N  32998  djaclN  34156  dihoml4c  34396  dochdmj1  34410  djhcl  34420  dochexmidlem4  34483  mapd1o  34668  mapdin  34682  elrfi  34988  elrfirn  34989  elrfirn2  34990  ismrcd1  34992  istopclsd  34994  isnacs2  35000  mrefg3  35002  isnacs3  35004  diophrw  35053  diophin  35067  aomclem2  35363  islmodfg  35377  lsmfgcl  35382  lmhmfgima  35392  lmhmfgsplit  35394  lmhmlnmsplit  35395  pwfi2f1o  35406  pwfi2f1oOLD  35407  hbt  35443  acsfn1p  35512  fiinfi  35624  trrelind  35644  rp-imass  35751  onfrALTlem2  36342  onfrALTlem2VD  36720  islptre  36993  sumnnodd  37004  limclner  37025  cncfuni  37057  fouriersw  37382  rngcbas  38284  rngchomfval  38285  rngccofval  38289  dfrngc2  38291  rnghmsscmap2  38292  rnghmsscmap  38293  rngcsect  38299  funcrngcsetc  38317  ringcbas  38330  ringchomfval  38331  ringccofval  38335  dfringc2  38337  rhmsscmap2  38338  rhmsscmap  38339  rhmsscrnghm  38345  ringcsect  38350  funcringcsetc  38354  funcringcsetcALTV2lem9  38363  fldc  38402  fldhmsubc  38403  rngcrescrhm  38404  rhmsubclem1  38405  fldcALTV  38421  fldhmsubcALTV  38422  rngcrescrhmALTV  38423  rhmsubcALTVlem1  38424
  Copyright terms: Public domain W3C validator