Theorem elinel2 4163

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  elin2d  4166  nel2nelin  4169  eldmeldmressn  6025  onfr  6401  partfun  6683  fvcofneq  7089  offres  7980  fsplitfpar  8113  ressuppss  8179  frrlem4  8286  frrlem11  8293  frrlem12  8294  smores3  8340  erdisj  8752  dffi2  9383  r0weon  9996  fodomfi2  10044  ackbij1lem6  10207  ackbij1lem9  10210  ackbij1lem10  10211  ackbij1lem11  10212  ackbij1lem18  10219  isfin1-3  10370  dedekindle  11374  uzdisj  13625  nn0disj  13672  rlimres  15609  lo1res  15610  ackbijnn  15882  bitsinv2  16501  bitsf1ocnv  16502  smueqlem  16548  prmrec  16982  isstruct2  17209  isacs2  17709  isdrs2  18362  isacs3lem  18598  subrngpropd  20653  subrgpropd  20693  rnghmsubcsetclem2  20717  rhmsubcsetclem2  20746  rhmsubcrngclem2  20752  sralmod  21286  basdif0  23079  clsval2  23176  mreclatdemoBAD  23222  restfpw  23305  fincmp  23519  discmp  23524  uncmp  23529  cmpfi  23534  bwth  23536  iunconn  23554  1stcrest  23579  infil  23989  alexsublem  24170  alexsubALTlem3  24175  tsmsfbas  24254  tsmsgsum  24265  tsmssubm  24269  tsmsres  24270  tsmsf1o  24271  tsmsmhm  24272  tsmsadd  24273  tsmsxplem1  24279  tsmsxp  24281  blres  24557  reconnlem2  24954  xrge0tsms  24961  ncvsge0  25281  cphsscph  25379  cfilres  25424  ioombl1lem4  25689  mbfadd  25789  mbfsub  25790  mbfmul  25854  itg2cnlem2  25890  bddmulibl  25967  ellimc2  26005  fsumvma2  27344  vmasum  27346  chpchtsum  27349  chebbnd1lem1  27599  dirith2  27658  uhgrspansubgrlem  29581  disjin2  32873  xrge0tsmsd  33334  prsdm  34249  prsrn  34250  pibt2  37951  heicant  38194  mndoisexid  38408  eqvreldisj  39237  eldisjsim2  39474  fiinfi  44191  ismnushort  44903  restuni3  45728  disjinfi  45802  inmap  45817  iocopn  46128  icoopn  46133  icomnfinre  46160  uzinico  46167  islpcn  46245  lptre2pt  46246  limcresiooub  46248  limcresioolb  46249  limclner  46257  limsupmnflem  46326  limsupresxr  46372  liminfresxr  46373  liminfvalxr  46389  icccncfext  46493  stoweidlem39  46645  stoweidlem50  46656  stoweidlem57  46663  fourierdlem32  46745  fourierdlem33  46746  fourierdlem48  46760  fourierdlem49  46761  fourierdlem71  46783  fourierdlem80  46792  qndenserrnbllem  46900  sge0rnre  46970  sge0z  46981  sge0tsms  46986  sge0cl  46987  sge0f1o  46988  sge0fsum  46993  sge0sup  46997  sge0rnbnd  46999  sge0ltfirp  47006  sge0resplit  47012  sge0le  47013  sge0split  47015  sge0iunmptlemre  47021  sge0ltfirpmpt2  47032  sge0isum  47033  sge0xaddlem1  47039  sge0xaddlem2  47040  sge0pnffsumgt  47048  sge0gtfsumgt  47049  sge0uzfsumgt  47050  sge0seq  47052  sge0reuz  47053  meadjiunlem  47071  caragendifcl  47120  omeiunltfirp  47125  carageniuncllem2  47128  caratheodorylem2  47133  hspmbllem2  47233  pimiooltgt  47316  pimdecfgtioc  47321  pimincfltioc  47322  pimdecfgtioo  47323  pimincfltioo  47324  sssmf  47344  smfaddlem1  47369  smfaddlem2  47370  smfadd  47371  mbfpsssmf  47389  smfmullem4  47400  smfmul  47401  smfdiv  47403  smfsuplem1  47417  smfliminflem  47436  fmtno4prm  48216