Theorem elinel2 4099

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091

This theorem is used by:  elin2d  4102  nel2nelin  4105  eldmeldmressn  6013  onfr  6402  partfun  6686  fvcofneq  7093  offres  7995  fsplitfpar  8129  ressuppss  8200  frrlem4  8307  frrlem11  8314  frrlem12  8315  smores3  8361  erdisj  8775  dffi2  9415  r0weon  10091  fodomfi2  10139  ackbij1lem6  10302  ackbij1lem9  10305  ackbij1lem10  10306  ackbij1lem11  10307  ackbij1lem18  10314  isfin1-3  10464  dedekindle  11474  uzdisj  13731  nn0disj  13778  rlimres  15725  lo1res  15726  ackbijnn  15997  bitsinv2  16613  bitsf1ocnv  16614  smueqlem  16660  prmrec  17100  isstruct2  17327  isacs2  17827  isdrs2  18480  isacs3lem  18716  subrngpropd  20820  subrgpropd  20860  rnghmsubcsetclem2  20884  rhmsubcsetclem2  20913  rhmsubcrngclem2  20919  sralmod  21462  basdif0  23271  clsval2  23368  mreclatdemoBAD  23414  restfpw  23497  fincmp  23711  discmp  23716  uncmp  23721  cmpfi  23726  bwth  23728  iunconn  23746  1stcrest  23771  infil  24182  alexsublem  24363  alexsubALTlem3  24368  tsmsfbas  24447  tsmsgsum  24458  tsmssubm  24462  tsmsres  24463  tsmsf1o  24464  tsmsmhm  24465  tsmsadd  24466  tsmsxplem1  24472  tsmsxp  24474  blres  24750  reconnlem2  25147  xrge0tsms  25154  ncvsge0  25474  cphsscph  25572  cfilres  25617  ioombl1lem4  25882  mbfadd  25982  mbfsub  25983  mbfmul  26047  itg2cnlem2  26083  bddmulibl  26159  ellimc2  26197  fsumvma2  27541  vmasum  27543  chpchtsum  27546  chebbnd1lem1  27796  dirith2  27855  uhgrspansubgrlem  29871  disjin2  33181  xrge0tsmsd  33634  prsdm  34546  prsrn  34547  pibt2  38341  heicant  38574  mndoisexid  38804  eqvreldisj  39631  eldisjsim2  39868  fiinfi  44574  ismnushort  45285  hfstructfun  46026  rnhfstructsshf  46027  restuni3  46133  disjinfi  46207  inmap  46222  iocopn  46532  icoopn  46537  icomnfinre  46564  uzinico  46571  islpcn  46649  lptre2pt  46650  limcresiooub  46652  limcresioolb  46653  limclner  46661  limsupmnflem  46730  limsupresxr  46776  liminfresxr  46777  liminfvalxr  46793  icccncfext  46897  stoweidlem39  47049  stoweidlem50  47060  stoweidlem57  47067  fourierdlem32  47149  fourierdlem33  47150  fourierdlem48  47164  fourierdlem49  47165  fourierdlem71  47187  fourierdlem80  47196  qndenserrnbllem  47304  sge0rnre  47374  sge0z  47385  sge0tsms  47390  sge0cl  47391  sge0f1o  47392  sge0fsum  47397  sge0sup  47401  sge0rnbnd  47403  sge0ltfirp  47410  sge0resplit  47416  sge0le  47417  sge0split  47419  sge0iunmptlemre  47425  sge0ltfirpmpt2  47436  sge0isum  47437  sge0xaddlem1  47443  sge0xaddlem2  47444  sge0pnffsumgt  47452  sge0gtfsumgt  47453  sge0uzfsumgt  47454  sge0seq  47456  sge0reuz  47457  meadjiunlem  47475  caragendifcl  47524  omeiunltfirp  47529  carageniuncllem2  47532  caratheodorylem2  47537  hspmbllem2  47637  pimiooltgt  47720  pimdecfgtioc  47725  pimincfltioc  47726  pimdecfgtioo  47727  pimincfltioo  47728  sssmf  47748  smfaddlem1  47773  smfaddlem2  47774  smfadd  47775  mbfpsssmf  47793  smfmullem4  47804  smfmul  47805  smfdiv  47807  smfsuplem1  47821  smfliminflem  47840  fmtno4prm  48660