Theorem elinel1 4171

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

Syntax hints:   → wi 4   ∈ wcel 2110   ∩ cin 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942

This theorem is referenced by:  elin1d  4174  inss1  4204  predel  6159  fvcofneq  6853  wfrlem4  7952  erdisj  8335  f1opwfi  8822  fival  8870  fi0  8878  dffi2  8881  elfiun  8888  epfrs  9167  r0weon  9432  fodomfi2  9480  ackbij1lem6  9641  ackbij1lem9  9644  ackbij1lem10  9645  ackbij1lem11  9646  fin23lem24  9738  fin23lem26  9741  isfin1-3  9802  canthp1lem2  10069  dedekindle  10798  uzdisj  12974  nn0disj  13017  lo1resb  14915  rlimresb  14916  o1resb  14917  ackbijnn  15177  prmreclem2  16247  isacs2  16918  acsfn  16924  isdrs2  17543  isacs3lem  17770  psssdm2  17819  resscntz  18456  mplind  20276  clsval2  21652  mreclatdemoBAD  21698  ordtrest  21804  fincmp  21995  discmp  22000  uncmp  22005  ptcnplem  22223  txkgen  22254  infil  22465  hauspwpwf1  22589  alexsubALTlem3  22651  alexsubALTlem4  22652  blbas  23034  blres  23035  xrge0tsms  23436  nmhmcn  23718  ncvsge0  23751  cphsscph  23848  mbfadd  24256  mbfsub  24257  i1fima2  24274  i1fd  24276  mbfmul  24321  bddmulibl  24433  limcun  24487  pilem2  25034  rlimcnp2  25538  xrlimcnp  25540  ppiprm  25722  chtprm  25724  prmorcht  25749  rplogsumlem2  26055  dchrisum0re  26083  uhgrspansubgrlem  27066  disjin  30330  xrge0tsmsd  30687  eulerpartgbij  31625  frrlem4  33121  frrlem12  33129  pibt2  34692  eqvreldisj  35843  fiinfi  39925  gneispace  40477  elpwinss  41304  restuni3  41377  nel1nelin  41408  disjinfi  41447  inmap  41465  iocopn  41789  icoopn  41794  icomnfinre  41821  uzinico  41829  islpcn  41913  lptre2pt  41914  limcresiooub  41916  limcresioolb  41917  limsupmnflem  41994  limsupresxr  42040  liminfresxr  42041  liminfvalxr  42057  liminf0  42067  icccncfext  42163  stoweidlem39  42318  stoweidlem50  42329  stoweidlem57  42336  fourierdlem32  42418  fourierdlem33  42419  fourierdlem48  42433  fourierdlem49  42434  fourierdlem71  42456  sge0rnre  42640  sge00  42652  sge0tsms  42656  sge0cl  42657  sge0fsum  42663  sge0sup  42667  sge0less  42668  sge0gerp  42671  sge0resplit  42682  sge0split  42685  sge0iunmptlemre  42691  caragendifcl  42790  hoiqssbllem3  42900  hspmbllem2  42903  pimiooltgt  42983  pimdecfgtioc  42987  pimincfltioc  42988  pimdecfgtioo  42989  pimincfltioo  42990  sssmf  43009  smfaddlem1  43033  smfaddlem2  43034  smfadd  43035  mbfpsssmf  43053  smfmul  43064  smfdiv  43066  smfsuplem1  43079  smfliminflem  43098  fmtno4prm  43731  rngcid  44244  ringcid  44290  rhmsubclem3  44353  rhmsubcALTVlem3  44371