Theorem elinel1 4172

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943

This theorem is referenced by:  elin1d  4175  inss1  4205  predel  6165  fvcofneq  6859  wfrlem4  7958  erdisj  8341  f1opwfi  8828  fival  8876  fi0  8884  dffi2  8887  elfiun  8894  epfrs  9173  r0weon  9438  fodomfi2  9486  ackbij1lem6  9647  ackbij1lem9  9650  ackbij1lem10  9651  ackbij1lem11  9652  fin23lem24  9744  fin23lem26  9747  isfin1-3  9808  canthp1lem2  10075  dedekindle  10804  uzdisj  12981  nn0disj  13024  lo1resb  14921  rlimresb  14922  o1resb  14923  ackbijnn  15183  prmreclem2  16253  isacs2  16924  acsfn  16930  isdrs2  17549  isacs3lem  17776  psssdm2  17825  resscntz  18462  mplind  20282  clsval2  21658  mreclatdemoBAD  21704  ordtrest  21810  fincmp  22001  discmp  22006  uncmp  22011  ptcnplem  22229  txkgen  22260  infil  22471  hauspwpwf1  22595  alexsubALTlem3  22657  alexsubALTlem4  22658  blbas  23040  blres  23041  xrge0tsms  23442  nmhmcn  23724  ncvsge0  23757  cphsscph  23854  mbfadd  24262  mbfsub  24263  i1fima2  24280  i1fd  24282  mbfmul  24327  bddmulibl  24439  limcun  24493  pilem2  25040  rlimcnp2  25544  xrlimcnp  25546  ppiprm  25728  chtprm  25730  prmorcht  25755  rplogsumlem2  26061  dchrisum0re  26089  uhgrspansubgrlem  27072  disjin  30336  xrge0tsmsd  30692  eulerpartgbij  31630  frrlem4  33126  frrlem12  33134  pibt2  34701  eqvreldisj  35864  fiinfi  39952  gneispace  40504  elpwinss  41331  restuni3  41404  nel1nelin  41435  disjinfi  41474  inmap  41492  iocopn  41816  icoopn  41821  icomnfinre  41848  uzinico  41856  islpcn  41940  lptre2pt  41941  limcresiooub  41943  limcresioolb  41944  limsupmnflem  42021  limsupresxr  42067  liminfresxr  42068  liminfvalxr  42084  liminf0  42094  icccncfext  42190  stoweidlem39  42344  stoweidlem50  42355  stoweidlem57  42362  fourierdlem32  42444  fourierdlem33  42445  fourierdlem48  42459  fourierdlem49  42460  fourierdlem71  42482  sge0rnre  42666  sge00  42678  sge0tsms  42682  sge0cl  42683  sge0fsum  42689  sge0sup  42693  sge0less  42694  sge0gerp  42697  sge0resplit  42708  sge0split  42711  sge0iunmptlemre  42717  caragendifcl  42816  hoiqssbllem3  42926  hspmbllem2  42929  pimiooltgt  43009  pimdecfgtioc  43013  pimincfltioc  43014  pimdecfgtioo  43015  pimincfltioo  43016  sssmf  43035  smfaddlem1  43059  smfaddlem2  43060  smfadd  43061  mbfpsssmf  43079  smfmul  43090  smfdiv  43092  smfsuplem1  43105  smfliminflem  43124  fmtno4prm  43757  rngcid  44270  ringcid  44316  rhmsubclem3  44379  rhmsubcALTVlem3  44397