Theorem elinel2 4155

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

Syntax hints:   → wi 4   ∈ wcel 2143   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  elin2d  4158  nel2nelin  4161  eldmeldmressn  6024  onfr  6400  partfun  6682  fvcofneq  7088  offres  7976  fsplitfpar  8109  ressuppss  8175  frrlem4  8282  frrlem11  8289  frrlem12  8290  smores3  8336  erdisj  8748  dffi2  9379  r0weon  9992  fodomfi2  10040  ackbij1lem6  10203  ackbij1lem9  10206  ackbij1lem10  10207  ackbij1lem11  10208  ackbij1lem18  10215  isfin1-3  10365  dedekindle  11369  uzdisj  13621  nn0disj  13668  rlimres  15605  lo1res  15606  ackbijnn  15878  bitsinv2  16496  bitsf1ocnv  16497  smueqlem  16543  prmrec  16977  isstruct2  17204  isacs2  17704  isdrs2  18357  isacs3lem  18593  subrngpropd  20667  subrgpropd  20707  rnghmsubcsetclem2  20731  rhmsubcsetclem2  20760  rhmsubcrngclem2  20766  sralmod  21308  basdif0  23110  clsval2  23207  mreclatdemoBAD  23253  restfpw  23336  fincmp  23550  discmp  23555  uncmp  23560  cmpfi  23565  bwth  23567  iunconn  23585  1stcrest  23610  infil  24020  alexsublem  24201  alexsubALTlem3  24206  tsmsfbas  24285  tsmsgsum  24296  tsmssubm  24300  tsmsres  24301  tsmsf1o  24302  tsmsmhm  24303  tsmsadd  24304  tsmsxplem1  24310  tsmsxp  24312  blres  24588  reconnlem2  24985  xrge0tsms  24992  ncvsge0  25312  cphsscph  25410  cfilres  25455  ioombl1lem4  25720  mbfadd  25820  mbfsub  25821  mbfmul  25885  itg2cnlem2  25921  bddmulibl  25998  ellimc2  26036  fsumvma2  27378  vmasum  27380  chpchtsum  27383  chebbnd1lem1  27633  dirith2  27692  uhgrspansubgrlem  29640  disjin2  32932  xrge0tsmsd  33393  prsdm  34304  prsrn  34305  pibt2  38083  heicant  38326  mndoisexid  38540  eqvreldisj  39367  eldisjsim2  39604  fiinfi  44319  ismnushort  45031  restuni3  45856  disjinfi  45930  inmap  45945  iocopn  46256  icoopn  46261  icomnfinre  46288  uzinico  46295  islpcn  46373  lptre2pt  46374  limcresiooub  46376  limcresioolb  46377  limclner  46385  limsupmnflem  46454  limsupresxr  46500  liminfresxr  46501  liminfvalxr  46517  icccncfext  46621  stoweidlem39  46773  stoweidlem50  46784  stoweidlem57  46791  fourierdlem32  46873  fourierdlem33  46874  fourierdlem48  46888  fourierdlem49  46889  fourierdlem71  46911  fourierdlem80  46920  qndenserrnbllem  47028  sge0rnre  47098  sge0z  47109  sge0tsms  47114  sge0cl  47115  sge0f1o  47116  sge0fsum  47121  sge0sup  47125  sge0rnbnd  47127  sge0ltfirp  47134  sge0resplit  47140  sge0le  47141  sge0split  47143  sge0iunmptlemre  47149  sge0ltfirpmpt2  47160  sge0isum  47161  sge0xaddlem1  47167  sge0xaddlem2  47168  sge0pnffsumgt  47176  sge0gtfsumgt  47177  sge0uzfsumgt  47178  sge0seq  47180  sge0reuz  47181  meadjiunlem  47199  caragendifcl  47248  omeiunltfirp  47253  carageniuncllem2  47256  caratheodorylem2  47261  hspmbllem2  47361  pimiooltgt  47444  pimdecfgtioc  47449  pimincfltioc  47450  pimdecfgtioo  47451  pimincfltioo  47452  sssmf  47472  smfaddlem1  47497  smfaddlem2  47498  smfadd  47499  mbfpsssmf  47517  smfmullem4  47528  smfmul  47529  smfdiv  47531  smfsuplem1  47545  smfliminflem  47564  fmtno4prm  48347