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

Theorem inss1 3817
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 elinel1 3783 . 2 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
21ssriv 3592 1 (𝐴𝐵) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cin 3559  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-in 3567  df-ss 3574
This theorem is referenced by:  inss2  3818  ssinss1  3825  unabs  3838  nssinpss  3840  dfin4  3849  inv1  3948  disjdif  4018  uniintsn  4486  wefrc  5078  relin1  5207  resss  5391  resmpt3  5419  cnvcnvss  5558  predss  5656  ordtri3or  5724  onfr  5732  ordelinel  5794  ordelinelOLD  5795  funin  5933  funimass2  5940  fnresin1  5973  fnres  5975  fresin  6040  fresaun  6042  fresaunres2  6043  nfvres  6191  ssimaex  6230  fneqeql2  6292  funiunfv  6471  isoini2  6554  ofrfval  6870  ofval  6871  ofrval  6872  off  6877  ofres  6878  ofco  6882  fparlem3  7239  fparlem4  7240  wfrlem4  7378  smores  7409  smores2  7411  tfrlem5  7436  pmresg  7845  sbthlem7  8036  sbthcl  8042  infi  8144  imafi  8219  ixpfi2  8224  unifpw  8229  f1opwfi  8230  fival  8278  fi0  8286  dffi2  8289  elfiun  8296  dffi3  8297  marypha1lem  8299  ordtypelem3  8385  ordtypelem4  8386  ordtypelem6  8388  ordtypelem7  8389  ordtypelem8  8390  wdomima2g  8451  epfrs  8567  tskwe  8736  r0weon  8795  fodomfi2  8843  infpwfien  8845  ackbij1lem6  9007  ackbij1lem9  9010  ackbij1lem10  9011  ackbij1lem11  9012  ackbij1lem15  9016  ackbij1lem16  9017  fin23lem24  9104  fin23lem26  9107  fin23lem23  9108  fin23lem22  9109  fin23lem19  9118  isfin1-3  9168  ttukeylem6  9296  brdom3  9310  brdom5  9311  brdom4  9312  imadomg  9316  fpwwe2lem12  9423  canthp1lem2  9435  wunin  9495  tskin  9541  gruima  9584  ingru  9597  gruina  9600  grur1a  9601  nqerf  9712  nqerrel  9714  dedekindle  10161  hashun3  13129  hashin  13155  hashdif  13157  xptrrel  13669  rexanuz  14035  limsupgle  14158  rlimres  14239  lo1res  14240  lo1resb  14245  rlimresb  14246  o1resb  14247  lo1eq  14249  rlimeq  14250  o1of2  14293  o1rlimmul  14299  isercolllem2  14346  isercolllem3  14347  isercoll  14348  ackbijnn  14504  incexclem  14512  incexc  14513  bitsinvp1  15114  sadcaddlem  15122  sadadd2lem  15124  sadadd3  15126  sadaddlem  15131  sadasslem  15135  sadeq  15137  bitsres  15138  smuval2  15147  smupval  15153  smueqlem  15155  smumul  15158  ramub2  15661  ramub1lem2  15674  fvsetsid  15830  ressinbas  15876  ressress  15878  submre  16205  submrc  16228  isacs2  16254  isacs1i  16258  mreacs  16259  acsfn  16260  invss  16361  sscres  16423  coffth  16536  catcisolem  16696  catciso  16697  catcoppccl  16698  catcfuccl  16699  catcxpccl  16787  isdrs2  16879  isacs3lem  17106  isacs5lem  17109  acsfiindd  17117  psss  17154  psssdm2  17155  tsrss  17163  tsrdir  17178  resscntz  17704  sylow2a  17974  lsmmod  18028  frgpnabllem2  18217  gsumzres  18250  gsumzaddlem  18261  dprddisj2  18378  ablfac1eu  18412  ablfac2  18428  isunit  18597  lspextmo  18996  2idlval  19173  aspsubrg  19271  psrbagsn  19435  mplind  19442  zringlpirlem2  19773  pjfval  19990  pjpm  19992  ofco2  20197  basdif0  20697  tgval2  20700  eltg3  20706  tgcl  20713  tgdom  20722  tgidm  20724  ppttop  20751  epttop  20753  ntropn  20793  ntrin  20805  mretopd  20836  mreclatdemoBAD  20840  neiptoptop  20875  restbas  20902  restfpw  20923  neitr  20924  restcls  20925  ordtrest  20946  subbascn  20998  cncls  21018  cnpresti  21032  cnprest  21033  fincmp  21136  cmpsublem  21142  cmpsub  21143  fiuncmp  21147  indisconn  21161  connsub  21164  cnconn  21165  iunconnlem  21170  clsconn  21173  conncompclo  21178  islly2  21227  cldllycmp  21238  kgentopon  21281  llycmpkgen2  21293  1stckgenlem  21296  ptbasfi  21324  txcls  21347  txcnp  21363  ptcnplem  21364  txcnmpt  21367  txcmplem2  21385  hausdiag  21388  txkgen  21395  xkopt  21398  xkococnlem  21402  txconn  21432  qtoptop2  21442  basqtop  21454  tgqtop  21455  kqnrmlem1  21486  kqnrmlem2  21487  nrmhmph  21537  fbssfi  21581  filin  21598  infil  21607  fbasrn  21628  fgtr  21634  ufprim  21653  flimrest  21727  hauspwpwf1  21731  txflf  21750  fclsrest  21768  alexsubALTlem3  21793  alexsubALTlem4  21794  ptcmplem5  21800  tsmsres  21887  tsmsxplem1  21896  ustund  21965  trust  21973  utoptop  21978  restutop  21981  cfiluweak  22039  xmetres  22109  metres  22110  blin2  22174  blbas  22175  blres  22176  setsmstopn  22223  met2ndci  22267  metrest  22269  ressxms  22270  tgioo  22539  xrsmopn  22555  zdis  22559  reconnlem1  22569  reconnlem2  22570  xrge0tsms  22577  cnheibor  22694  lebnum  22703  nmoleub2lem  22854  nmoleub2lem2  22856  nmhmcn  22860  tchcph  22976  cfilresi  23033  cfilres  23034  caussi  23035  causs  23036  relcmpcmet  23055  minveclem4a  23141  minveclem4  23143  ismbl2  23235  cmmbl  23242  nulmbl2  23244  unmbl  23245  shftmbl  23246  volinun  23254  voliunlem1  23258  voliunlem2  23259  ioombl1lem4  23269  ioombl1  23270  ioorcl  23285  uniioombllem2  23291  uniioombllem3  23293  uniioombllem4  23294  uniioombllem5  23295  uniioombl  23297  volivth  23315  vitalilem3  23319  vitalilem4  23320  vitalilem5  23321  vitali  23322  mbfadd  23368  mbfsub  23369  i1fima2  23386  i1fd  23388  i1fadd  23402  itg1addlem2  23404  itg1addlem4  23406  itg1addlem5  23407  itg1climres  23421  mbfmul  23433  itg2splitlem  23455  itg2split  23456  limcresi  23589  limciun  23598  limcun  23599  dvreslem  23613  dvres2lem  23614  dvres  23615  dvres3a  23618  dvaddbr  23641  dvmulbr  23642  dvfsumle  23722  dvfsumabs  23724  ig1peu  23869  taylfvallem1  24049  pilem2  24144  pilem3  24145  rlimcnp2  24627  xrlimcnp  24629  ppisval  24764  ppifi  24766  ppiprm  24811  ppinprm  24812  chtprm  24813  chtnprm  24814  chtdif  24818  efchtdvds  24819  ppidif  24823  ppiltx  24837  prmorcht  24838  ppiub  24863  chtlepsi  24865  chtleppi  24869  pclogsum  24874  vmasum  24875  chpval2  24877  chpchtsum  24878  chpub  24879  2sqlem8  25085  chebbnd1lem1  25092  chtppilimlem1  25096  rplogsumlem2  25108  rpvmasum2  25135  dchrisum0re  25136  rplogsum  25150  dirith2  25151  axtgcgrrflx  25295  axtgcgrid  25296  axtgsegcon  25297  axtg5seg  25298  axtgbtwnid  25299  axtgpasch  25300  axtgcont1  25301  perpcom  25542  perpneq  25543  ragperp  25546  phnv  27557  minvecolem2  27619  minvecolem3  27620  minvecolem5  27625  minvecolem6  27626  minvecolem7  27627  hlimcaui  27981  chdmm1i  28224  chabs1  28263  chabs2  28264  ledii  28283  lejdii  28285  pjoml4i  28334  cmbr3i  28347  cmbr4i  28348  cmm1i  28353  osumcor2i  28391  3oalem4  28412  pjssmii  28428  pjocini  28445  pjini  28446  mayete3i  28475  riesz4  28811  riesz1  28812  cnlnadjeui  28824  cnlnadjeu  28825  cnlnssadj  28827  nmopadjlei  28835  pjin1i  28939  pjclem1  28942  stji1i  28989  stm1i  28990  dmdbr2  29050  ssmd1  29058  mdslj2i  29067  mdsl2bi  29070  mdslmd1lem1  29072  mdslmd2i  29077  atomli  29129  atcvat4i  29144  sumdmdlem2  29166  dmdbr5ati  29169  dmdbr6ati  29170  dmdbr7ati  29171  disjxpin  29287  imadifxp  29300  off2  29326  ffsrn  29388  gsummptres  29611  xrge0tsmsd  29612  ordtrestNEW  29791  qqhnm  29858  qqhcn  29859  rrhre  29889  indf1ofs  29911  esumval  29931  esumel  29932  gsumesum  29944  esumlub  29945  esumcst  29948  esumfsup  29955  esumpcvgval  29963  esumcvg  29971  sigainb  30022  ldgenpisyslem1  30049  measinb2  30109  sibfinima  30224  sibfof  30225  eulerpartlemelr  30242  eulerpartlem1  30252  eulerpartgbij  30257  eulerpartlemgvv  30261  eulerpartlemgu  30262  eulerpartlemgs2  30265  sseqf  30277  ballotlemfelz  30375  ballotlemfp1  30376  bnj1292  30647  connpconn  30978  iccllysconn  30993  cvmsss2  31017  cvmcov2  31018  cvmopnlem  31021  cvmliftmolem2  31025  cvmliftlem15  31041  cvmlift2lem12  31057  mvrsfpw  31164  msrf  31200  elmsta  31206  mthmpps  31240  nepss  31361  dfon2lem4  31445  frrlem4  31537  txpss3v  31680  fixssdm  31708  fixssrn  31709  limitssson  31713  fneer  32043  neibastop1  32049  neibastop2lem  32050  filnetlem3  32070  ontopbas  32122  bj-disj2r  32713  bj-restpw  32735  bj-ablssgrp  32810  taupilemrplb  32838  taupilem2  32840  taupi  32841  ptrest  33079  poimirlem29  33109  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  mbfposadd  33128  sstotbnd2  33244  ssbnd  33258  heibor1lem  33279  heiborlem1  33281  heiborlem3  33283  heiborlem5  33285  heiborlem6  33286  heiborlem10  33290  heibor  33291  opidonOLD  33322  exidcl  33346  flddivrng  33469  lshpinN  33795  lcvexchlem5  33844  pmodlem2  34652  pmod1i  34653  pmodN  34655  osumcllem7N  34767  pexmidlem4N  34778  pl42lem3N  34786  djaclN  35944  dihoml4c  36184  dochdmj1  36198  djhcl  36208  dochexmidlem4  36271  mapd1o  36456  mapdin  36470  elrfi  36776  elrfirn  36777  elrfirn2  36778  ismrcd1  36780  istopclsd  36782  isnacs2  36788  mrefg3  36790  isnacs3  36792  diophrw  36841  diophin  36855  aomclem2  37144  islmodfg  37158  lsmfgcl  37163  lmhmfgima  37173  lmhmfgsplit  37175  lmhmlnmsplit  37176  pwfi2f1o  37185  hbt  37220  acsfn1p  37289  elinintrab  37403  trrelind  37477  rp-imass  37586  clsk3nimkb  37859  isotone2  37868  onfrALTlem2  38282  onfrALTlem2VD  38647  unirestss  38832  inmap  38910  fnfvimad  38969  fsumiunss  39243  islptre  39287  sumnnodd  39298  limclner  39319  cncfuni  39434  ismbl3  39540  ismbl4  39547  fouriersw  39785  qndenserrnbllem  39851  salincl  39880  salgencntex  39898  sge0less  39946  sge0resplit  39960  sge0split  39963  sge0iunmptlemre  39969  carageniuncllem1  40072  carageniuncllem2  40073  caragenel2d  40083  hspmbllem3  40179  hspmbl  40180  ovolval2lem  40194  sssmf  40284  smfaddlem1  40308  smflimlem2  40317  smflimlem3  40318  smflimlem4  40319  smfres  40334  smfmullem4  40338  smfsuplem1  40354  rngcbas  41283  rngchomfval  41284  rngccofval  41288  dfrngc2  41290  rnghmsscmap2  41291  rnghmsscmap  41292  rngcsect  41298  funcrngcsetc  41316  ringcbas  41329  ringchomfval  41330  ringccofval  41334  dfringc2  41336  rhmsscmap2  41337  rhmsscmap  41338  rhmsscrnghm  41344  ringcsect  41349  funcringcsetc  41353  funcringcsetcALTV2lem9  41362  fldc  41401  fldhmsubc  41402  rngcrescrhm  41403  rhmsubclem1  41404  fldcALTV  41419  fldhmsubcALTV  41420  rngcrescrhmALTV  41421  rhmsubcALTVlem1  41422  setrec2fun  41762  setrec2lem1  41763
  Copyright terms: Public domain W3C validator