Theorem elinel1 4224

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 3992	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simplbi 497	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  elin1d  4227  inss1  4258  predel  6353  fvcofneq  7127  frrlem4  8330  frrlem12  8338  wfrlem4OLD  8368  erdisj  8817  f1opwfi  9426  fival  9481  fi0  9489  dffi2  9492  elfiun  9499  epfrs  9800  r0weon  10081  fodomfi2  10129  ackbij1lem6  10293  ackbij1lem9  10296  ackbij1lem10  10297  ackbij1lem11  10298  fin23lem24  10391  fin23lem26  10394  isfin1-3  10455  canthp1lem2  10722  dedekindle  11454  uzdisj  13657  nn0disj  13701  lo1resb  15610  rlimresb  15611  o1resb  15612  ackbijnn  15876  prmreclem2  16964  isacs2  17711  acsfn  17717  isdrs2  18376  isacs3lem  18612  psssdm2  18651  resscntz  19373  rngcid  20657  ringcid  20686  rhmsubclem3  20709  mplind  22117  clsval2  23079  mreclatdemoBAD  23125  ordtrest  23231  fincmp  23422  discmp  23427  uncmp  23432  ptcnplem  23650  txkgen  23681  infil  23892  hauspwpwf1  24016  alexsubALTlem3  24078  alexsubALTlem4  24079  blbas  24461  blres  24462  xrge0tsms  24875  nmhmcn  25172  ncvsge0  25206  cphsscph  25304  mbfadd  25715  mbfsub  25716  i1fima2  25733  i1fd  25735  mbfmul  25781  bddmulibl  25894  limcun  25950  pilem2  26514  rlimcnp2  27027  xrlimcnp  27029  ppiprm  27212  chtprm  27214  prmorcht  27239  rplogsumlem2  27547  dchrisum0re  27575  uhgrspansubgrlem  29325  disjin  32608  xrge0tsmsd  33041  eulerpartgbij  34337  pibt2  37383  eqvreldisj  38570  mhpind  42549  fiinfi  43535  gneispace  44096  ismnushort  44270  elpwinss  44951  restuni3  45020  nel1nelin  45048  disjinfi  45099  inmap  45116  iocopn  45438  icoopn  45443  icomnfinre  45470  uzinico  45478  islpcn  45560  lptre2pt  45561  limcresiooub  45563  limcresioolb  45564  limsupmnflem  45641  limsupresxr  45687  liminfresxr  45688  liminfvalxr  45704  liminf0  45714  icccncfext  45808  stoweidlem39  45960  stoweidlem50  45971  stoweidlem57  45978  fourierdlem32  46060  fourierdlem33  46061  fourierdlem48  46075  fourierdlem49  46076  fourierdlem71  46098  sge0rnre  46285  sge00  46297  sge0tsms  46301  sge0cl  46302  sge0fsum  46308  sge0sup  46312  sge0less  46313  sge0gerp  46316  sge0resplit  46327  sge0split  46330  sge0iunmptlemre  46336  caragendifcl  46435  hoiqssbllem3  46545  hspmbllem2  46548  pimiooltgt  46631  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  sssmf  46659  smfaddlem1  46684  smfaddlem2  46685  smfadd  46686  mbfpsssmf  46704  smfmul  46716  smfdiv  46718  smfsuplem1  46732  smfliminflem  46751  fmtno4prm  47449  rhmsubcALTVlem3  48006