Theorem elinel1 4142

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  elin1d  4145  nel1nelin  4148  inss1  4178  predel  6280  fvcofneq  7040  frrlem4  8233  frrlem12  8241  erdisj  8695  f1opwfi  9260  fival  9319  fi0  9327  dffi2  9330  elfiun  9337  epfrs  9646  r0weon  9928  fodomfi2  9976  ackbij1lem6  10140  ackbij1lem9  10143  ackbij1lem10  10144  ackbij1lem11  10145  fin23lem24  10238  fin23lem26  10241  isfin1-3  10302  canthp1lem2  10570  dedekindle  11304  uzdisj  13545  nn0disj  13592  lo1resb  15520  rlimresb  15521  o1resb  15522  ackbijnn  15787  prmreclem2  16882  isacs2  17613  acsfn  17619  isdrs2  18266  isacs3lem  18502  psssdm2  18541  resscntz  19302  rngcid  20606  ringcid  20635  rhmsubclem3  20658  mplind  22061  clsval2  23028  mreclatdemoBAD  23074  ordtrest  23180  fincmp  23371  discmp  23376  uncmp  23381  ptcnplem  23599  txkgen  23630  infil  23841  hauspwpwf1  23965  alexsubALTlem3  24027  alexsubALTlem4  24028  blbas  24408  blres  24409  xrge0tsms  24813  nmhmcn  25100  ncvsge0  25133  cphsscph  25231  mbfadd  25641  mbfsub  25642  i1fima2  25659  i1fd  25661  mbfmul  25706  bddmulibl  25819  limcun  25875  pilem2  26433  rlimcnp2  26946  xrlimcnp  26948  ppiprm  27131  chtprm  27133  prmorcht  27158  rplogsumlem2  27465  dchrisum0re  27493  uhgrspansubgrlem  29376  disjin  32674  xrge0tsmsd  33152  eulerpartgbij  34535  dfttc4  36731  pibt2  37750  dfadjliftmap2  38795  dfblockliftmap2  38799  eqvreldisj  39036  mhpind  43044  fiinfi  44021  gneispace  44582  ismnushort  44749  elpwinss  45501  restuni3  45569  disjinfi  45643  inmap  45659  iocopn  45971  icoopn  45976  icomnfinre  46003  uzinico  46010  islpcn  46088  lptre2pt  46089  limcresiooub  46091  limcresioolb  46092  limsupmnflem  46169  limsupresxr  46215  liminfresxr  46216  liminfvalxr  46232  liminf0  46242  icccncfext  46336  stoweidlem39  46488  stoweidlem50  46499  stoweidlem57  46506  fourierdlem32  46588  fourierdlem33  46589  fourierdlem48  46603  fourierdlem49  46604  fourierdlem71  46626  sge0rnre  46813  sge00  46825  sge0tsms  46829  sge0cl  46830  sge0fsum  46836  sge0sup  46840  sge0less  46841  sge0gerp  46844  sge0resplit  46855  sge0split  46858  sge0iunmptlemre  46864  caragendifcl  46963  hoiqssbllem3  47073  hspmbllem2  47076  pimiooltgt  47159  pimdecfgtioc  47164  pimincfltioc  47165  pimdecfgtioo  47166  pimincfltioo  47167  sssmf  47187  smfaddlem1  47212  smfaddlem2  47213  smfadd  47214  mbfpsssmf  47232  smfmul  47244  smfdiv  47246  smfsuplem1  47260  smfliminflem  47279  nthrucw  47335  fmtno4prm  48053  rhmsubcALTVlem3  48774