Theorem elinel1 4191

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

Syntax hints:   → wi 4   ∈ wcel 2099   ∩ cin 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952

This theorem is referenced by:  elin1d  4194  inss1  4224  predel  6320  fvcofneq  7097  frrlem4  8288  frrlem12  8296  wfrlem4OLD  8326  erdisj  8771  f1opwfi  9374  fival  9429  fi0  9437  dffi2  9440  elfiun  9447  epfrs  9748  r0weon  10029  fodomfi2  10077  ackbij1lem6  10242  ackbij1lem9  10245  ackbij1lem10  10246  ackbij1lem11  10247  fin23lem24  10339  fin23lem26  10342  isfin1-3  10403  canthp1lem2  10670  dedekindle  11402  uzdisj  13600  nn0disj  13643  lo1resb  15534  rlimresb  15535  o1resb  15536  ackbijnn  15800  prmreclem2  16879  isacs2  17626  acsfn  17632  isdrs2  18291  isacs3lem  18527  psssdm2  18566  resscntz  19277  rngcid  20561  ringcid  20590  rhmsubclem3  20613  mplind  22007  clsval2  22947  mreclatdemoBAD  22993  ordtrest  23099  fincmp  23290  discmp  23295  uncmp  23300  ptcnplem  23518  txkgen  23549  infil  23760  hauspwpwf1  23884  alexsubALTlem3  23946  alexsubALTlem4  23947  blbas  24329  blres  24330  xrge0tsms  24743  nmhmcn  25040  ncvsge0  25074  cphsscph  25172  mbfadd  25583  mbfsub  25584  i1fima2  25601  i1fd  25603  mbfmul  25649  bddmulibl  25761  limcun  25817  pilem2  26382  rlimcnp2  26891  xrlimcnp  26893  ppiprm  27076  chtprm  27078  prmorcht  27103  rplogsumlem2  27411  dchrisum0re  27439  uhgrspansubgrlem  29096  disjin  32369  xrge0tsmsd  32765  eulerpartgbij  33986  pibt2  36890  eqvreldisj  38080  mhpind  41821  fiinfi  42997  gneispace  43558  ismnushort  43732  elpwinss  44407  restuni3  44478  nel1nelin  44506  disjinfi  44559  inmap  44576  iocopn  44899  icoopn  44904  icomnfinre  44931  uzinico  44939  islpcn  45021  lptre2pt  45022  limcresiooub  45024  limcresioolb  45025  limsupmnflem  45102  limsupresxr  45148  liminfresxr  45149  liminfvalxr  45165  liminf0  45175  icccncfext  45269  stoweidlem39  45421  stoweidlem50  45432  stoweidlem57  45439  fourierdlem32  45521  fourierdlem33  45522  fourierdlem48  45536  fourierdlem49  45537  fourierdlem71  45559  sge0rnre  45746  sge00  45758  sge0tsms  45762  sge0cl  45763  sge0fsum  45769  sge0sup  45773  sge0less  45774  sge0gerp  45777  sge0resplit  45788  sge0split  45791  sge0iunmptlemre  45797  caragendifcl  45896  hoiqssbllem3  46006  hspmbllem2  46009  pimiooltgt  46092  pimdecfgtioc  46097  pimincfltioc  46098  pimdecfgtioo  46099  pimincfltioo  46100  sssmf  46120  smfaddlem1  46145  smfaddlem2  46146  smfadd  46147  mbfpsssmf  46165  smfmul  46177  smfdiv  46179  smfsuplem1  46193  smfliminflem  46212  fmtno4prm  46909  rhmsubcALTVlem3  47339

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »