Theorem elinel2 4154

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
elinel2	⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Proof of Theorem elinel2

Step	Hyp	Ref	Expression
1		elin 3917	. 2 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶))
2	1	simprbi 496	1 ⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  elin2d  4157  nel2nelin  4160  eldmeldmressn  5984  onfr  6356  partfun  6639  fvcofneq  7038  offres  7927  fsplitfpar  8060  ressuppss  8125  frrlem4  8231  frrlem11  8238  frrlem12  8239  smores3  8285  erdisj  8692  dffi2  9326  r0weon  9922  fodomfi2  9970  ackbij1lem6  10134  ackbij1lem9  10137  ackbij1lem10  10138  ackbij1lem11  10139  ackbij1lem18  10146  isfin1-3  10296  dedekindle  11297  uzdisj  13513  nn0disj  13560  rlimres  15481  lo1res  15482  ackbijnn  15751  bitsinv2  16370  bitsf1ocnv  16371  smueqlem  16417  prmrec  16850  isstruct2  17076  isacs2  17576  isdrs2  18229  isacs3lem  18465  subrngpropd  20501  subrgpropd  20541  rnghmsubcsetclem2  20565  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  sralmod  21139  basdif0  22897  clsval2  22994  mreclatdemoBAD  23040  restfpw  23123  fincmp  23337  discmp  23342  uncmp  23347  cmpfi  23352  bwth  23354  iunconn  23372  1stcrest  23397  infil  23807  alexsublem  23988  alexsubALTlem3  23993  tsmsfbas  24072  tsmsgsum  24083  tsmssubm  24087  tsmsres  24088  tsmsf1o  24089  tsmsmhm  24090  tsmsadd  24091  tsmsxplem1  24097  tsmsxp  24099  blres  24375  reconnlem2  24772  xrge0tsms  24779  ncvsge0  25109  cphsscph  25207  cfilres  25252  ioombl1lem4  25518  mbfadd  25618  mbfsub  25619  mbfmul  25683  itg2cnlem2  25719  bddmulibl  25796  ellimc2  25834  fsumvma2  27181  vmasum  27183  chpchtsum  27186  chebbnd1lem1  27436  dirith2  27495  uhgrspansubgrlem  29363  disjin2  32662  xrge0tsmsd  33155  prsdm  34071  prsrn  34072  pibt2  37622  heicant  37856  mndoisexid  38070  eqvreldisj  38881  fiinfi  43824  ismnushort  44552  restuni3  45372  disjinfi  45446  inmap  45463  iocopn  45776  icoopn  45781  icomnfinre  45808  uzinico  45815  islpcn  45893  lptre2pt  45894  limcresiooub  45896  limcresioolb  45897  limclner  45905  limsupmnflem  45974  limsupresxr  46020  liminfresxr  46021  liminfvalxr  46037  icccncfext  46141  stoweidlem39  46293  stoweidlem50  46304  stoweidlem57  46311  fourierdlem32  46393  fourierdlem33  46394  fourierdlem48  46408  fourierdlem49  46409  fourierdlem71  46431  fourierdlem80  46440  qndenserrnbllem  46548  sge0rnre  46618  sge0z  46629  sge0tsms  46634  sge0cl  46635  sge0f1o  46636  sge0fsum  46641  sge0sup  46645  sge0rnbnd  46647  sge0ltfirp  46654  sge0resplit  46660  sge0le  46661  sge0split  46663  sge0iunmptlemre  46669  sge0ltfirpmpt2  46680  sge0isum  46681  sge0xaddlem1  46687  sge0xaddlem2  46688  sge0pnffsumgt  46696  sge0gtfsumgt  46697  sge0uzfsumgt  46698  sge0seq  46700  sge0reuz  46701  meadjiunlem  46719  caragendifcl  46768  omeiunltfirp  46773  carageniuncllem2  46776  caratheodorylem2  46781  hspmbllem2  46881  pimiooltgt  46964  pimdecfgtioc  46969  pimincfltioc  46970  pimdecfgtioo  46971  pimincfltioo  46972  sssmf  46992  smfaddlem1  47017  smfaddlem2  47018  smfadd  47019  mbfpsssmf  47037  smfmullem4  47048  smfmul  47049  smfdiv  47051  smfsuplem1  47065  smfliminflem  47084  fmtno4prm  47831