Theorem elinel1 4141

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  elin1d  4144  nel1nelin  4147  inss1  4177  predel  6285  fvcofneq  7045  frrlem4  8239  frrlem12  8247  erdisj  8701  f1opwfi  9266  fival  9325  fi0  9333  dffi2  9336  elfiun  9343  epfrs  9652  r0weon  9934  fodomfi2  9982  ackbij1lem6  10146  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1lem11  10151  fin23lem24  10244  fin23lem26  10247  isfin1-3  10308  canthp1lem2  10576  dedekindle  11310  uzdisj  13551  nn0disj  13598  lo1resb  15526  rlimresb  15527  o1resb  15528  ackbijnn  15793  prmreclem2  16888  isacs2  17619  acsfn  17625  isdrs2  18272  isacs3lem  18508  psssdm2  18547  resscntz  19308  rngcid  20612  ringcid  20641  rhmsubclem3  20664  mplind  22048  clsval2  23015  mreclatdemoBAD  23061  ordtrest  23167  fincmp  23358  discmp  23363  uncmp  23368  ptcnplem  23586  txkgen  23617  infil  23828  hauspwpwf1  23952  alexsubALTlem3  24014  alexsubALTlem4  24015  blbas  24395  blres  24396  xrge0tsms  24800  nmhmcn  25087  ncvsge0  25120  cphsscph  25218  mbfadd  25628  mbfsub  25629  i1fima2  25646  i1fd  25648  mbfmul  25693  bddmulibl  25806  limcun  25862  pilem2  26417  rlimcnp2  26930  xrlimcnp  26932  ppiprm  27114  chtprm  27116  prmorcht  27141  rplogsumlem2  27448  dchrisum0re  27476  uhgrspansubgrlem  29359  disjin  32656  xrge0tsmsd  33134  eulerpartgbij  34516  dfttc4  36712  pibt2  37733  dfadjliftmap2  38778  dfblockliftmap2  38782  eqvreldisj  39019  mhpind  43027  fiinfi  44000  gneispace  44561  ismnushort  44728  elpwinss  45480  restuni3  45548  disjinfi  45622  inmap  45638  iocopn  45950  icoopn  45955  icomnfinre  45982  uzinico  45989  islpcn  46067  lptre2pt  46068  limcresiooub  46070  limcresioolb  46071  limsupmnflem  46148  limsupresxr  46194  liminfresxr  46195  liminfvalxr  46211  liminf0  46221  icccncfext  46315  stoweidlem39  46467  stoweidlem50  46478  stoweidlem57  46485  fourierdlem32  46567  fourierdlem33  46568  fourierdlem48  46582  fourierdlem49  46583  fourierdlem71  46605  sge0rnre  46792  sge00  46804  sge0tsms  46808  sge0cl  46809  sge0fsum  46815  sge0sup  46819  sge0less  46820  sge0gerp  46823  sge0resplit  46834  sge0split  46837  sge0iunmptlemre  46843  caragendifcl  46942  hoiqssbllem3  47052  hspmbllem2  47055  pimiooltgt  47138  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  sssmf  47166  smfaddlem1  47191  smfaddlem2  47192  smfadd  47193  mbfpsssmf  47211  smfmul  47223  smfdiv  47225  smfsuplem1  47239  smfliminflem  47258  nthrucw  47316  fmtno4prm  48038  rhmsubcALTVlem3  48759