Theorem elinel2 4094

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

Syntax hints:   → wi 4   ∈ wcel 2081   ∩ cin 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3866

This theorem is referenced by:  elin2d  4097  eldmeldmressn  5777  onfr  6105  fvcofneq  6724  offres  7540  ressuppss  7700  wfrlem4  7809  smores3  7842  erdisj  8191  dffi2  8733  r0weon  9284  fodomfi2  9332  ackbij1lem6  9493  ackbij1lem9  9496  ackbij1lem10  9497  ackbij1lem11  9498  ackbij1lem18  9505  isfin1-3  9654  dedekindle  10651  uzdisj  12830  nn0disj  12873  rlimres  14749  lo1res  14750  ackbijnn  15016  bitsinv2  15625  bitsf1ocnv  15626  smueqlem  15672  prmrec  16087  isstruct2  16322  isacs2  16753  isdrs2  17378  isacs3lem  17605  subrgpropd  19260  sralmod  19649  basdif0  21245  clsval2  21342  mreclatdemoBAD  21388  restfpw  21471  fincmp  21685  discmp  21690  uncmp  21695  cmpfi  21700  bwth  21702  iunconn  21720  1stcrest  21745  infil  22155  alexsublem  22336  alexsubALTlem3  22341  tsmsfbas  22419  tsmsgsum  22430  tsmssubm  22434  tsmsres  22435  tsmsf1o  22436  tsmsmhm  22437  tsmsadd  22438  tsmsxplem1  22444  tsmsxp  22446  blres  22724  reconnlem2  23118  xrge0tsms  23125  ncvsge0  23440  cphsscph  23537  cfilres  23582  ioombl1lem4  23845  mbfadd  23945  mbfsub  23946  mbfmul  24010  itg2cnlem2  24046  bddmulibl  24122  ellimc2  24158  fsumvma2  25472  vmasum  25474  chpchtsum  25477  chebbnd1lem1  25727  dirith2  25786  uhgrspansubgrlem  26755  disjin2  30027  partfun  30111  xrge0tsmsd  30503  prsdm  30774  prsrn  30775  frrlem4  32735  frrlem11  32742  frrlem12  32743  pibt2  34229  heicant  34458  mndoisexid  34679  eqvreldisj  35380  fiinfi  39417  restuni3  40924  nel2nelin  40955  disjinfi  40994  inmap  41012  iocopn  41338  icoopn  41343  icomnfinre  41370  uzinico  41378  islpcn  41462  lptre2pt  41463  limcresiooub  41465  limcresioolb  41466  limclner  41474  limsupmnflem  41543  limsupresxr  41589  liminfresxr  41590  liminfvalxr  41606  icccncfext  41711  stoweidlem39  41866  stoweidlem50  41877  stoweidlem57  41884  fourierdlem32  41966  fourierdlem33  41967  fourierdlem48  41981  fourierdlem49  41982  fourierdlem71  42004  fourierdlem80  42013  qndenserrnbllem  42121  sge0rnre  42188  sge0z  42199  sge0tsms  42204  sge0cl  42205  sge0f1o  42206  sge0fsum  42211  sge0sup  42215  sge0rnbnd  42217  sge0ltfirp  42224  sge0resplit  42230  sge0le  42231  sge0split  42233  sge0iunmptlemre  42239  sge0ltfirpmpt2  42250  sge0isum  42251  sge0xaddlem1  42257  sge0xaddlem2  42258  sge0pnffsumgt  42266  sge0gtfsumgt  42267  sge0uzfsumgt  42268  sge0seq  42270  sge0reuz  42271  meadjiunlem  42289  caragendifcl  42338  omeiunltfirp  42343  carageniuncllem2  42346  caratheodorylem2  42351  hspmbllem2  42451  pimiooltgt  42531  pimdecfgtioc  42535  pimincfltioc  42536  pimdecfgtioo  42537  pimincfltioo  42538  sssmf  42557  smfaddlem1  42581  smfaddlem2  42582  smfadd  42583  mbfpsssmf  42601  smfmullem4  42611  smfmul  42612  smfdiv  42614  smfsuplem1  42627  smfliminflem  42646  fmtno4prm  43219  rnghmsubcsetclem2  43725  rhmsubcsetclem2  43771  rhmsubcrngclem2  43777