Theorem elinel1 4162

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  elin1d  4165  nel1nelin  4168  inss1  4197  predel  6323  fvcofneq  7089  frrlem4  8286  frrlem12  8294  erdisj  8752  f1opwfi  9313  fival  9372  fi0  9380  dffi2  9383  elfiun  9390  epfrs  9700  r0weon  9996  fodomfi2  10044  ackbij1lem6  10207  ackbij1lem9  10210  ackbij1lem10  10211  ackbij1lem11  10212  fin23lem24  10306  fin23lem26  10309  isfin1-3  10370  canthp1lem2  10638  dedekindle  11374  uzdisj  13625  nn0disj  13672  lo1resb  15615  rlimresb  15616  o1resb  15617  ackbijnn  15882  prmreclem2  16977  isacs2  17709  acsfn  17715  isdrs2  18362  isacs3lem  18598  psssdm2  18637  resscntz  19403  rngcid  20720  ringcid  20749  rhmsubclem3  20772  mplind  22190  clsval2  23176  mreclatdemoBAD  23222  ordtrest  23328  fincmp  23519  discmp  23524  uncmp  23529  ptcnplem  23747  txkgen  23778  infil  23989  hauspwpwf1  24113  alexsubALTlem3  24175  alexsubALTlem4  24176  blbas  24556  blres  24557  xrge0tsms  24961  nmhmcn  25248  ncvsge0  25281  cphsscph  25379  mbfadd  25789  mbfsub  25790  i1fima2  25807  i1fd  25809  mbfmul  25854  bddmulibl  25967  limcun  26023  pilem2  26581  rlimcnp2  27097  xrlimcnp  27099  ppiprm  27281  chtprm  27283  prmorcht  27308  rplogsumlem2  27615  dchrisum0re  27643  uhgrspansubgrlem  29581  disjin  32872  xrge0tsmsd  33334  eulerpartgbij  34707  dfttc4  36964  pibt2  37985  dfadjliftmap2  39030  dfblockliftmap2  39034  eqvreldisj  39271  mhpind  43252  fiinfi  44225  gneispace  44786  ismnushort  44937  elpwinss  45695  restuni3  45762  disjinfi  45836  inmap  45851  iocopn  46162  icoopn  46167  icomnfinre  46194  uzinico  46201  islpcn  46279  lptre2pt  46280  limcresiooub  46282  limcresioolb  46283  limsupmnflem  46360  limsupresxr  46406  liminfresxr  46407  liminfvalxr  46423  liminf0  46433  icccncfext  46527  stoweidlem39  46679  stoweidlem50  46690  stoweidlem57  46697  fourierdlem32  46779  fourierdlem33  46780  fourierdlem48  46794  fourierdlem49  46795  fourierdlem71  46817  sge0rnre  47004  sge00  47016  sge0tsms  47020  sge0cl  47021  sge0fsum  47027  sge0sup  47031  sge0less  47032  sge0gerp  47035  sge0resplit  47046  sge0split  47049  sge0iunmptlemre  47055  caragendifcl  47154  hoiqssbllem3  47264  hspmbllem2  47267  pimiooltgt  47350  pimdecfgtioc  47355  pimincfltioc  47356  pimdecfgtioo  47357  pimincfltioo  47358  sssmf  47378  smfaddlem1  47403  smfaddlem2  47404  smfadd  47405  mbfpsssmf  47423  smfmul  47435  smfdiv  47437  smfsuplem1  47451  smfliminflem  47470  nthrucw  47528  fmtno4prm  48250  rhmsubcALTVlem3  48971