Theorem elinel1 4160

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918

This theorem is referenced by:  elin1d  4163  nel1nelin  4166  inss1  4196  predel  6282  fvcofneq  7047  frrlem4  8245  frrlem12  8253  erdisj  8705  f1opwfi  9283  fival  9339  fi0  9347  dffi2  9350  elfiun  9357  epfrs  9660  r0weon  9941  fodomfi2  9989  ackbij1lem6  10153  ackbij1lem9  10156  ackbij1lem10  10157  ackbij1lem11  10158  fin23lem24  10251  fin23lem26  10254  isfin1-3  10315  canthp1lem2  10582  dedekindle  11314  uzdisj  13534  nn0disj  13581  lo1resb  15506  rlimresb  15507  o1resb  15508  ackbijnn  15770  prmreclem2  16864  isacs2  17594  acsfn  17600  isdrs2  18247  isacs3lem  18483  psssdm2  18522  resscntz  19247  rngcid  20555  ringcid  20584  rhmsubclem3  20607  mplind  22010  clsval2  22970  mreclatdemoBAD  23016  ordtrest  23122  fincmp  23313  discmp  23318  uncmp  23323  ptcnplem  23541  txkgen  23572  infil  23783  hauspwpwf1  23907  alexsubALTlem3  23969  alexsubALTlem4  23970  blbas  24351  blres  24352  xrge0tsms  24756  nmhmcn  25053  ncvsge0  25086  cphsscph  25184  mbfadd  25595  mbfsub  25596  i1fima2  25613  i1fd  25615  mbfmul  25660  bddmulibl  25773  limcun  25829  pilem2  26395  rlimcnp2  26909  xrlimcnp  26911  ppiprm  27094  chtprm  27096  prmorcht  27121  rplogsumlem2  27429  dchrisum0re  27457  uhgrspansubgrlem  29270  disjin  32565  xrge0tsmsd  33045  eulerpartgbij  34356  pibt2  37398  eqvreldisj  38598  mhpind  42575  fiinfi  43555  gneispace  44116  ismnushort  44283  elpwinss  45036  restuni3  45105  disjinfi  45179  inmap  45196  iocopn  45511  icoopn  45516  icomnfinre  45543  uzinico  45550  islpcn  45630  lptre2pt  45631  limcresiooub  45633  limcresioolb  45634  limsupmnflem  45711  limsupresxr  45757  liminfresxr  45758  liminfvalxr  45774  liminf0  45784  icccncfext  45878  stoweidlem39  46030  stoweidlem50  46041  stoweidlem57  46048  fourierdlem32  46130  fourierdlem33  46131  fourierdlem48  46145  fourierdlem49  46146  fourierdlem71  46168  sge0rnre  46355  sge00  46367  sge0tsms  46371  sge0cl  46372  sge0fsum  46378  sge0sup  46382  sge0less  46383  sge0gerp  46386  sge0resplit  46397  sge0split  46400  sge0iunmptlemre  46406  caragendifcl  46505  hoiqssbllem3  46615  hspmbllem2  46618  pimiooltgt  46701  pimdecfgtioc  46706  pimincfltioc  46707  pimdecfgtioo  46708  pimincfltioo  46709  sssmf  46729  smfaddlem1  46754  smfaddlem2  46755  smfadd  46756  mbfpsssmf  46774  smfmul  46786  smfdiv  46788  smfsuplem1  46802  smfliminflem  46821  fmtno4prm  47569  rhmsubcALTVlem3  48264