Theorem elinel2 4142

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  elin2d  4145  nel2nelin  4148  eldmeldmressn  5990  onfr  6362  partfun  6645  fvcofneq  7045  offres  7936  fsplitfpar  8068  ressuppss  8133  frrlem4  8239  frrlem11  8246  frrlem12  8247  smores3  8293  erdisj  8701  dffi2  9336  r0weon  9934  fodomfi2  9982  ackbij1lem6  10146  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1lem11  10151  ackbij1lem18  10158  isfin1-3  10308  dedekindle  11310  uzdisj  13551  nn0disj  13598  rlimres  15520  lo1res  15521  ackbijnn  15793  bitsinv2  16412  bitsf1ocnv  16413  smueqlem  16459  prmrec  16893  isstruct2  17119  isacs2  17619  isdrs2  18272  isacs3lem  18508  subrngpropd  20545  subrgpropd  20585  rnghmsubcsetclem2  20609  rhmsubcsetclem2  20638  rhmsubcrngclem2  20644  sralmod  21182  basdif0  22918  clsval2  23015  mreclatdemoBAD  23061  restfpw  23144  fincmp  23358  discmp  23363  uncmp  23368  cmpfi  23373  bwth  23375  iunconn  23393  1stcrest  23418  infil  23828  alexsublem  24009  alexsubALTlem3  24014  tsmsfbas  24093  tsmsgsum  24104  tsmssubm  24108  tsmsres  24109  tsmsf1o  24110  tsmsmhm  24111  tsmsadd  24112  tsmsxplem1  24118  tsmsxp  24120  blres  24396  reconnlem2  24793  xrge0tsms  24800  ncvsge0  25120  cphsscph  25218  cfilres  25263  ioombl1lem4  25528  mbfadd  25628  mbfsub  25629  mbfmul  25693  itg2cnlem2  25729  bddmulibl  25806  ellimc2  25844  fsumvma2  27177  vmasum  27179  chpchtsum  27182  chebbnd1lem1  27432  dirith2  27491  uhgrspansubgrlem  29359  disjin2  32657  xrge0tsmsd  33134  prsdm  34058  prsrn  34059  pibt2  37733  heicant  37976  mndoisexid  38190  eqvreldisj  39019  eldisjsim2  39256  fiinfi  44000  ismnushort  44728  restuni3  45548  disjinfi  45622  inmap  45638  iocopn  45950  icoopn  45955  icomnfinre  45982  uzinico  45989  islpcn  46067  lptre2pt  46068  limcresiooub  46070  limcresioolb  46071  limclner  46079  limsupmnflem  46148  limsupresxr  46194  liminfresxr  46195  liminfvalxr  46211  icccncfext  46315  stoweidlem39  46467  stoweidlem50  46478  stoweidlem57  46485  fourierdlem32  46567  fourierdlem33  46568  fourierdlem48  46582  fourierdlem49  46583  fourierdlem71  46605  fourierdlem80  46614  qndenserrnbllem  46722  sge0rnre  46792  sge0z  46803  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0fsum  46815  sge0sup  46819  sge0rnbnd  46821  sge0ltfirp  46828  sge0resplit  46834  sge0le  46835  sge0split  46837  sge0iunmptlemre  46843  sge0ltfirpmpt2  46854  sge0isum  46855  sge0xaddlem1  46861  sge0xaddlem2  46862  sge0pnffsumgt  46870  sge0gtfsumgt  46871  sge0uzfsumgt  46872  sge0seq  46874  sge0reuz  46875  meadjiunlem  46893  caragendifcl  46942  omeiunltfirp  46947  carageniuncllem2  46950  caratheodorylem2  46955  hspmbllem2  47055  pimiooltgt  47138  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  sssmf  47166  smfaddlem1  47191  smfaddlem2  47192  smfadd  47193  mbfpsssmf  47211  smfmullem4  47222  smfmul  47223  smfdiv  47225  smfsuplem1  47239  smfliminflem  47258  fmtno4prm  48038