Theorem inss1 4120

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		elinel1 4088	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3888	1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴

Syntax hints:   ∩ cin 3853   ⊆ wss 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-in 3861  df-ss 3869

This theorem is referenced by:  inss2  4121  ssinss1  4129  unabs  4146  nssinpss  4148  dfin4  4159  inv1  4262  disjdif  4329  uniintsn  4813  wefrc  5429  relin1  5563  resss  5751  resmpt3  5779  cnvcnvss  5919  predss  6022  ordtri3or  6090  onfr  6097  ordelinel  6156  funin  6292  funimass2  6299  fnresin1  6334  fnres  6336  fresin  6407  fresaun  6409  nfvres  6566  ssimaex  6607  fneqeql2  6673  fnfvimad  6852  funiunfv  6863  isoini2  6946  ofrfval  7266  ofval  7267  ofrval  7268  off  7273  ofres  7274  ofco  7278  fparlem3  7656  fparlem4  7657  wfrlem4OLD  7801  smores  7832  smores2  7834  tfrlem5  7859  pmresg  8275  sbthlem7  8470  sbthcl  8476  infi  8578  imafi  8653  ixpfi2  8658  unifpw  8663  elfiun  8730  dffi3  8731  marypha1lem  8733  ordtypelem6  8823  ordtypelem7  8824  ordtypelem8  8825  wdomima2g  8886  tskwe  9214  ackbij1lem15  9491  ackbij1lem16  9492  fin23lem23  9583  fin23lem22  9584  fin23lem19  9593  brdom3  9785  brdom5  9786  brdom4  9787  imadomg  9791  fpwwe2lem12  9898  canthp1lem2  9910  wunin  9970  tskin  10016  gruima  10059  ingru  10072  gruina  10075  grur1a  10076  nqerf  10187  nqerrel  10189  hashun3  13581  hashin  13608  hashdif  13610  xptrrel  14162  rexanuz  14527  limsupgle  14656  rlimres  14737  lo1res  14738  lo1resb  14743  rlimresb  14744  o1resb  14745  lo1eq  14747  rlimeq  14748  o1of2  14791  o1rlimmul  14797  isercolllem2  14844  isercolllem3  14845  isercoll  14846  incexclem  15012  incexc  15013  bitsinvp1  15619  sadcaddlem  15627  sadadd2lem  15629  sadadd3  15631  sadaddlem  15636  sadasslem  15640  sadeq  15642  bitsres  15643  smuval2  15652  smupval  15658  smueqlem  15660  smumul  15663  ramub2  16167  ramub1lem2  16180  fvsetsid  16332  ressinbas  16377  ressress  16379  submre  16693  isacs1i  16745  mreacs  16746  acsfn  16747  invss  16848  sscres  16910  catcisolem  17183  catciso  17184  isacs5lem  17596  psss  17641  tsrss  17650  tsrdir  17665  sylow2a  18462  lsmmod  18516  gsumzres  18738  gsumzaddlem  18749  dprddisj2  18866  ablfac1eu  18900  isunit  19085  acsfn1p  19256  lspextmo  19506  2idlval  19683  aspsubrg  19781  psrbagsn  19950  pjfval  20520  pjpm  20522  ofco2  20732  basdif0  21233  tgval2  21236  eltg3  21242  tgcl  21249  tgdom  21258  tgidm  21260  ppttop  21287  epttop  21289  ntropn  21329  ntrin  21341  mretopd  21372  neiptoptop  21411  restfpw  21459  neitr  21460  restcls  21461  cncls  21554  cnpresti  21568  cnprest  21569  cmpsublem  21679  cmpsub  21680  fiuncmp  21684  indisconn  21698  connsub  21701  iunconnlem  21707  islly2  21764  cldllycmp  21775  kgentopon  21818  ptbasfi  21861  ptcnplem  21901  txcnmpt  21904  txcmplem2  21922  hausdiag  21925  txkgen  21932  xkococnlem  21939  qtoptop2  21979  basqtop  21991  fbssfi  22117  filin  22134  infil  22143  fbasrn  22164  fgtr  22170  ufprim  22189  flimrest  22263  txflf  22286  fclsrest  22304  alexsubALTlem4  22330  tsmsres  22423  tsmsxplem1  22432  ustund  22501  trust  22509  utoptop  22514  restutop  22517  cfiluweak  22575  xmetres  22645  metres  22646  blin2  22710  setsmstopn  22759  metrest  22805  ressxms  22806  tgioo  23075  xrsmopn  23091  reconnlem1  23105  xrge0tsms  23113  tcphcph  23511  cfilresi  23569  cfilres  23570  caussi  23571  causs  23572  relcmpcmet  23592  minveclem4a  23704  ismbl2  23799  cmmbl  23806  nulmbl2  23808  unmbl  23809  shftmbl  23810  volinun  23818  voliunlem1  23822  voliunlem2  23823  ioombl1lem4  23833  ioombl1  23834  uniioombllem2  23855  uniioombllem3  23857  uniioombllem4  23858  uniioombllem5  23859  uniioombl  23861  volivth  23879  vitalilem3  23882  vitalilem4  23883  vitalilem5  23884  vitali  23885  mbfadd  23933  mbfsub  23934  i1fadd  23967  itg1addlem2  23969  itg1addlem4  23971  itg1addlem5  23972  itg1climres  23986  mbfmul  23998  itg2splitlem  24020  itg2split  24021  limcresi  24154  limciun  24163  dvreslem  24178  dvres2lem  24179  dvres  24180  dvres3a  24183  dvaddbr  24206  dvmulbr  24207  dvfsumle  24289  dvfsumabs  24291  ig1peu  24436  pilem2  24711  pilem3  24712  rlimcnp2  25214  ppisval  25351  ppifi  25353  ppiprm  25398  chtprm  25400  chtdif  25405  efchtdvds  25406  ppidif  25410  ppiltx  25424  prmorcht  25425  ppiub  25450  chtlepsi  25452  pclogsum  25461  vmasum  25462  chpval2  25464  chpub  25466  2sqlem8  25672  chebbnd1lem1  25715  chtppilimlem1  25719  rpvmasum2  25758  dchrisum0re  25759  rplogsum  25773  dirith2  25774  axtgcgrrflx  25918  axtgcgrid  25919  axtgsegcon  25920  axtg5seg  25921  axtgbtwnid  25922  axtgpasch  25923  axtgcont1  25924  phnv  28270  minvecolem2  28331  minvecolem3  28332  minvecolem5  28337  minvecolem6  28338  minvecolem7  28339  hlimcaui  28692  chdmm1i  28933  chabs1  28972  chabs2  28973  ledii  28992  lejdii  28994  pjoml4i  29043  cmbr3i  29056  cmbr4i  29057  cmm1i  29062  osumcor2i  29100  3oalem4  29121  pjssmii  29137  pjocini  29154  pjini  29155  mayete3i  29184  riesz4  29520  riesz1  29521  cnlnadjeui  29533  cnlnadjeu  29534  cnlnssadj  29536  nmopadjlei  29544  pjin1i  29648  pjclem1  29651  stji1i  29698  stm1i  29699  dmdbr2  29759  ssmd1  29767  mdslj2i  29776  mdsl2bi  29779  mdslmd1lem1  29781  mdslmd2i  29786  atomli  29838  atcvat4i  29853  sumdmdlem2  29875  dmdbr5ati  29878  dmdbr6ati  29879  dmdbr7ati  29880  disjxpin  30004  imadifxp  30017  off2  30051  ffsrn  30126  gsummptres  30459  xrge0tsmsd  30460  ordtrestNEW  30737  qqhnm  30804  qqhcn  30805  rrhre  30835  indsumin  30854  indf1ofs  30858  esumval  30878  esumel  30879  gsumesum  30891  esumlub  30892  esumcst  30895  esumfsup  30902  esumpcvgval  30910  esumcvg  30918  sigainb  30968  ldgenpisyslem1  30995  measinb2  31055  sibfinima  31170  sibfof  31171  eulerpartlemelr  31188  eulerpartlem1  31198  eulerpartgbij  31203  eulerpartlemgu  31208  eulerpartlemgs2  31211  sseqf  31223  ballotlemfelz  31321  ballotlemfp1  31322  reprinrn  31462  reprinfz1  31466  hgt750lemd  31492  bnj1292  31660  connpconn  32046  iccllysconn  32061  cvmsss2  32085  cvmcov2  32086  cvmopnlem  32089  cvmliftmolem2  32093  cvmliftlem15  32109  cvmlift2lem12  32125  mvrsfpw  32306  msrf  32342  elmsta  32348  mthmpps  32382  nepss  32501  dfon2lem4  32584  frrlem4  32680  frrlem13  32689  frrlem15  32696  nosupbnd1lem1  32762  nosupbnd2  32770  txpss3v  32893  fixssdm  32921  fixssrn  32922  limitssson  32926  fneer  33255  neibastop1  33261  neibastop2lem  33262  filnetlem3  33282  ontopbas  33329  bj-disj2r  33888  bj-restpw  33928  bj-discrmoore  33949  bj-fvsnun2  34042  bj-ablssgrp  34056  taupilemrplb  34078  taupilem2  34080  taupi  34081  ptrest  34368  poimirlem29  34398  mblfinlem3  34408  mblfinlem4  34409  ismblfin  34410  mbfposadd  34416  sstotbnd2  34530  ssbnd  34544  heibor1lem  34565  heiborlem1  34567  heiborlem3  34569  heiborlem5  34571  heiborlem6  34572  heiborlem10  34576  heibor  34577  opidonOLD  34608  exidcl  34632  flddivrng  34755  iss2  35083  xrnss3v  35105  refrelsredund2  35349  lshpinN  35606  lcvexchlem5  35655  pmodlem2  36464  pmod1i  36465  pmodN  36467  osumcllem7N  36579  pexmidlem4N  36590  pl42lem3N  36598  djaclN  37753  dihoml4c  37993  dochdmj1  38007  djhcl  38017  dochexmidlem4  38080  mapd1o  38265  mapdin  38279  elrfi  38726  elrfirn  38727  elrfirn2  38728  ismrcd1  38730  istopclsd  38732  isnacs2  38738  mrefg3  38740  isnacs3  38742  diophrw  38791  diophin  38805  aomclem2  39091  islmodfg  39105  lsmfgcl  39110  lmhmfgima  39120  lmhmfgsplit  39122  lmhmlnmsplit  39123  pwfi2f1o  39132  hbt  39166  harval3  39340  elinintrab  39373  trrelind  39446  rp-imass  39553  clsk3nimkb  39826  isotone2  39835  onfrALTlem2  40371  onfrALTlem2VD  40714  unirestss  40883  inmap  40965  fsumiunss  41352  islptre  41396  sumnnodd  41407  limclner  41428  liminfval4  41566  liminfval3  41567  cnrefiisplem  41606  cncfuni  41664  ismbl3  41767  ismbl4  41774  fouriersw  42012  qndenserrnbllem  42075  salincl  42104  salgencntex  42122  sge0less  42170  sge0resplit  42184  sge0split  42187  sge0iunmptlemre  42193  carageniuncllem1  42299  carageniuncllem2  42300  caragenel2d  42310  hspmbllem3  42406  hspmbl  42407  ovolval2lem  42421  sssmf  42511  smfaddlem1  42535  smflimlem2  42544  smflimlem3  42545  smflimlem4  42546  smfres  42561  smfmullem4  42565  smfsuplem1  42581  rngcbas  43668  rngchomfval  43669  rngccofval  43673  dfrngc2  43675  rnghmsscmap2  43676  rnghmsscmap  43677  rngcsect  43683  funcrngcsetc  43701  ringcbas  43714  ringchomfval  43715  ringccofval  43719  dfringc2  43721  rhmsscmap2  43722  rhmsscmap  43723  rhmsscrnghm  43729  ringcsect  43734  funcringcsetc  43738  funcringcsetcALTV2lem9  43747  fldc  43786  fldhmsubc  43787  rngcrescrhm  43788  rhmsubclem1  43789  fldcALTV  43804  fldhmsubcALTV  43805  rngcrescrhmALTV  43806  rhmsubcALTVlem1  43807  setrec2fun  44229  setrec2lem1  44230