Theorem elinel1 4154

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  elin1d  4157  nel1nelin  4160  inss1  4189  predel  6326  fvcofneq  7092  frrlem4  8292  frrlem12  8300  erdisj  8758  f1opwfi  9320  fival  9379  fi0  9387  dffi2  9390  elfiun  9397  epfrs  9707  r0weon  10012  fodomfi2  10060  ackbij1lem6  10223  ackbij1lem9  10226  ackbij1lem10  10227  ackbij1lem11  10228  fin23lem24  10321  fin23lem26  10324  isfin1-3  10385  canthp1lem2  10655  dedekindle  11391  uzdisj  13644  nn0disj  13691  lo1resb  15641  rlimresb  15642  o1resb  15643  ackbijnn  15907  prmreclem2  17001  isacs2  17733  acsfn  17739  isdrs2  18386  isacs3lem  18622  psssdm2  18661  resscntz  19449  rngcid  20786  ringcid  20815  rhmsubclem3  20838  mplind  22273  clsval2  23259  mreclatdemoBAD  23305  ordtrest  23411  fincmp  23602  discmp  23607  uncmp  23612  ptcnplem  23831  txkgen  23862  infil  24073  hauspwpwf1  24197  alexsubALTlem3  24259  alexsubALTlem4  24260  blbas  24640  blres  24641  xrge0tsms  25045  nmhmcn  25332  ncvsge0  25365  cphsscph  25463  mbfadd  25873  mbfsub  25874  i1fima2  25891  i1fd  25893  mbfmul  25938  bddmulibl  26051  limcun  26107  pilem2  26668  rlimcnp2  27184  xrlimcnp  27186  ppiprm  27368  chtprm  27370  prmorcht  27395  rplogsumlem2  27702  dchrisum0re  27730  uhgrspansubgrlem  29700  disjin  33004  xrge0tsmsd  33459  eulerpartgbij  34829  dfttc4  37100  pibt2  38122  dfadjliftmap2  39166  dfblockliftmap2  39170  eqvreldisj  39407  mhpind  43386  fiinfi  44359  gneispace  44920  ismnushort  45071  elpwinss  45829  restuni3  45896  disjinfi  45970  inmap  45985  iocopn  46296  icoopn  46301  icomnfinre  46328  uzinico  46335  islpcn  46413  lptre2pt  46414  limcresiooub  46416  limcresioolb  46417  limsupmnflem  46494  limsupresxr  46540  liminfresxr  46541  liminfvalxr  46557  liminf0  46567  icccncfext  46661  stoweidlem39  46813  stoweidlem50  46824  stoweidlem57  46831  fourierdlem32  46913  fourierdlem33  46914  fourierdlem48  46928  fourierdlem49  46929  fourierdlem71  46951  sge0rnre  47138  sge00  47150  sge0tsms  47154  sge0cl  47155  sge0fsum  47161  sge0sup  47165  sge0less  47166  sge0gerp  47169  sge0resplit  47180  sge0split  47183  sge0iunmptlemre  47189  caragendifcl  47288  hoiqssbllem3  47398  hspmbllem2  47401  pimiooltgt  47484  pimdecfgtioc  47489  pimincfltioc  47490  pimdecfgtioo  47491  pimincfltioo  47492  sssmf  47512  smfaddlem1  47537  smfaddlem2  47538  smfadd  47539  mbfpsssmf  47557  smfmul  47569  smfdiv  47571  smfsuplem1  47585  smfliminflem  47604  nthrucw  47667  fmtno4prm  48387  rhmsubcALTVlem3  49107