Theorem elinel1 4095

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

Syntax hints:   → wi 4   ∈ wcel 2080   ∩ cin 3860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-v 3438  df-in 3868

This theorem is referenced by:  elin1d  4098  inss1  4127  predel  6043  fvcofneq  6727  wfrlem4  7812  erdisj  8194  f1opwfi  8677  fival  8725  fi0  8733  dffi2  8736  elfiun  8743  epfrs  9022  r0weon  9287  fodomfi2  9335  ackbij1lem6  9496  ackbij1lem9  9499  ackbij1lem10  9500  ackbij1lem11  9501  fin23lem24  9593  fin23lem26  9596  isfin1-3  9657  canthp1lem2  9924  dedekindle  10653  uzdisj  12830  nn0disj  12873  lo1resb  14755  rlimresb  14756  o1resb  14757  ackbijnn  15016  prmreclem2  16082  isacs2  16753  acsfn  16759  isdrs2  17378  isacs3lem  17605  psssdm2  17654  resscntz  18203  mplind  19969  clsval2  21342  mreclatdemoBAD  21388  ordtrest  21494  fincmp  21685  discmp  21690  uncmp  21695  ptcnplem  21913  txkgen  21944  infil  22155  hauspwpwf1  22279  alexsubALTlem3  22341  alexsubALTlem4  22342  blbas  22723  blres  22724  xrge0tsms  23125  nmhmcn  23407  ncvsge0  23440  cphsscph  23537  mbfadd  23945  mbfsub  23946  i1fima2  23963  i1fd  23965  mbfmul  24010  bddmulibl  24122  limcun  24176  pilem2  24723  rlimcnp2  25226  xrlimcnp  25228  ppiprm  25410  chtprm  25412  prmorcht  25437  rplogsumlem2  25743  dchrisum0re  25771  uhgrspansubgrlem  26755  disjin  30018  xrge0tsmsd  30495  eulerpartgbij  31239  frrlem4  32729  frrlem12  32737  pibt2  34242  eqvreldisj  35393  fiinfi  39430  gneispace  39982  elpwinss  40863  restuni3  40937  nel1nelin  40967  disjinfi  41007  inmap  41025  iocopn  41351  icoopn  41356  icomnfinre  41383  uzinico  41391  islpcn  41475  lptre2pt  41476  limcresiooub  41478  limcresioolb  41479  limsupmnflem  41556  limsupresxr  41602  liminfresxr  41603  liminfvalxr  41619  liminf0  41629  icccncfext  41725  stoweidlem39  41880  stoweidlem50  41891  stoweidlem57  41898  fourierdlem32  41980  fourierdlem33  41981  fourierdlem48  41995  fourierdlem49  41996  fourierdlem71  42018  sge0rnre  42202  sge00  42214  sge0tsms  42218  sge0cl  42219  sge0fsum  42225  sge0sup  42229  sge0less  42230  sge0gerp  42233  sge0resplit  42244  sge0split  42247  sge0iunmptlemre  42253  caragendifcl  42352  hoiqssbllem3  42462  hspmbllem2  42465  pimiooltgt  42545  pimdecfgtioc  42549  pimincfltioc  42550  pimdecfgtioo  42551  pimincfltioo  42552  sssmf  42571  smfaddlem1  42595  smfaddlem2  42596  smfadd  42597  mbfpsssmf  42615  smfmul  42626  smfdiv  42628  smfsuplem1  42641  smfliminflem  42660  fmtno4prm  43233  rngcid  43742  ringcid  43788  rhmsubclem3  43851  rhmsubcALTVlem3  43869