Theorem elinel1 4196

Description: Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
elinel1	⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)

Proof of Theorem elinel1

Step	Hyp	Ref	Expression
1		elin 3965	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simplbi 499	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956

This theorem is referenced by:  elin1d  4199  inss1  4229  predel  6322  fvcofneq  7095  frrlem4  8274  frrlem12  8282  wfrlem4OLD  8312  erdisj  8755  f1opwfi  9356  fival  9407  fi0  9415  dffi2  9418  elfiun  9425  epfrs  9726  r0weon  10007  fodomfi2  10055  ackbij1lem6  10220  ackbij1lem9  10223  ackbij1lem10  10224  ackbij1lem11  10225  fin23lem24  10317  fin23lem26  10320  isfin1-3  10381  canthp1lem2  10648  dedekindle  11378  uzdisj  13574  nn0disj  13617  lo1resb  15508  rlimresb  15509  o1resb  15510  ackbijnn  15774  prmreclem2  16850  isacs2  17597  acsfn  17603  isdrs2  18259  isacs3lem  18495  psssdm2  18534  resscntz  19197  mplind  21631  clsval2  22554  mreclatdemoBAD  22600  ordtrest  22706  fincmp  22897  discmp  22902  uncmp  22907  ptcnplem  23125  txkgen  23156  infil  23367  hauspwpwf1  23491  alexsubALTlem3  23553  alexsubALTlem4  23554  blbas  23936  blres  23937  xrge0tsms  24350  nmhmcn  24636  ncvsge0  24670  cphsscph  24768  mbfadd  25178  mbfsub  25179  i1fima2  25196  i1fd  25198  mbfmul  25244  bddmulibl  25356  limcun  25412  pilem2  25964  rlimcnp2  26471  xrlimcnp  26473  ppiprm  26655  chtprm  26657  prmorcht  26682  rplogsumlem2  26988  dchrisum0re  27016  uhgrspansubgrlem  28547  disjin  31817  xrge0tsmsd  32209  eulerpartgbij  33371  pibt2  36298  eqvreldisj  37484  mhpind  41166  fiinfi  42324  gneispace  42885  ismnushort  43060  elpwinss  43736  restuni3  43807  nel1nelin  43835  disjinfi  43891  inmap  43908  iocopn  44233  icoopn  44238  icomnfinre  44265  uzinico  44273  islpcn  44355  lptre2pt  44356  limcresiooub  44358  limcresioolb  44359  limsupmnflem  44436  limsupresxr  44482  liminfresxr  44483  liminfvalxr  44499  liminf0  44509  icccncfext  44603  stoweidlem39  44755  stoweidlem50  44766  stoweidlem57  44773  fourierdlem32  44855  fourierdlem33  44856  fourierdlem48  44870  fourierdlem49  44871  fourierdlem71  44893  sge0rnre  45080  sge00  45092  sge0tsms  45096  sge0cl  45097  sge0fsum  45103  sge0sup  45107  sge0less  45108  sge0gerp  45111  sge0resplit  45122  sge0split  45125  sge0iunmptlemre  45131  caragendifcl  45230  hoiqssbllem3  45340  hspmbllem2  45343  pimiooltgt  45426  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  sssmf  45454  smfaddlem1  45479  smfaddlem2  45480  smfadd  45481  mbfpsssmf  45499  smfmul  45511  smfdiv  45513  smfsuplem1  45527  smfliminflem  45546  fmtno4prm  46243  rngcid  46877  ringcid  46923  rhmsubclem3  46986  rhmsubcALTVlem3  47004