Theorem elinel2 4225

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  elin2d  4228  eldmeldmressn  6054  onfr  6434  partfun  6727  fvcofneq  7127  offres  8024  fsplitfpar  8159  ressuppss  8224  frrlem4  8330  frrlem11  8337  frrlem12  8338  wfrlem4OLD  8368  smores3  8409  erdisj  8817  dffi2  9492  r0weon  10081  fodomfi2  10129  ackbij1lem6  10293  ackbij1lem9  10296  ackbij1lem10  10297  ackbij1lem11  10298  ackbij1lem18  10305  isfin1-3  10455  dedekindle  11454  uzdisj  13657  nn0disj  13701  rlimres  15604  lo1res  15605  ackbijnn  15876  bitsinv2  16489  bitsf1ocnv  16490  smueqlem  16536  prmrec  16969  isstruct2  17196  isacs2  17711  isdrs2  18376  isacs3lem  18612  subrngpropd  20594  subrgpropd  20636  rnghmsubcsetclem2  20654  rhmsubcsetclem2  20683  rhmsubcrngclem2  20689  sralmod  21217  basdif0  22981  clsval2  23079  mreclatdemoBAD  23125  restfpw  23208  fincmp  23422  discmp  23427  uncmp  23432  cmpfi  23437  bwth  23439  iunconn  23457  1stcrest  23482  infil  23892  alexsublem  24073  alexsubALTlem3  24078  tsmsfbas  24157  tsmsgsum  24168  tsmssubm  24172  tsmsres  24173  tsmsf1o  24174  tsmsmhm  24175  tsmsadd  24176  tsmsxplem1  24182  tsmsxp  24184  blres  24462  reconnlem2  24868  xrge0tsms  24875  ncvsge0  25206  cphsscph  25304  cfilres  25349  ioombl1lem4  25615  mbfadd  25715  mbfsub  25716  mbfmul  25781  itg2cnlem2  25817  bddmulibl  25894  ellimc2  25932  fsumvma2  27276  vmasum  27278  chpchtsum  27281  chebbnd1lem1  27531  dirith2  27590  uhgrspansubgrlem  29325  disjin2  32609  xrge0tsmsd  33041  prsdm  33860  prsrn  33861  pibt2  37383  heicant  37615  mndoisexid  37829  eqvreldisj  38570  fiinfi  43535  ismnushort  44270  restuni3  45020  nel2nelin  45049  disjinfi  45099  inmap  45116  iocopn  45438  icoopn  45443  icomnfinre  45470  uzinico  45478  islpcn  45560  lptre2pt  45561  limcresiooub  45563  limcresioolb  45564  limclner  45572  limsupmnflem  45641  limsupresxr  45687  liminfresxr  45688  liminfvalxr  45704  icccncfext  45808  stoweidlem39  45960  stoweidlem50  45971  stoweidlem57  45978  fourierdlem32  46060  fourierdlem33  46061  fourierdlem48  46075  fourierdlem49  46076  fourierdlem71  46098  fourierdlem80  46107  qndenserrnbllem  46215  sge0rnre  46285  sge0z  46296  sge0tsms  46301  sge0cl  46302  sge0f1o  46303  sge0fsum  46308  sge0sup  46312  sge0rnbnd  46314  sge0ltfirp  46321  sge0resplit  46327  sge0le  46328  sge0split  46330  sge0iunmptlemre  46336  sge0ltfirpmpt2  46347  sge0isum  46348  sge0xaddlem1  46354  sge0xaddlem2  46355  sge0pnffsumgt  46363  sge0gtfsumgt  46364  sge0uzfsumgt  46365  sge0seq  46367  sge0reuz  46368  meadjiunlem  46386  caragendifcl  46435  omeiunltfirp  46440  carageniuncllem2  46443  caratheodorylem2  46448  hspmbllem2  46548  pimiooltgt  46631  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  sssmf  46659  smfaddlem1  46684  smfaddlem2  46685  smfadd  46686  mbfpsssmf  46704  smfmullem4  46715  smfmul  46716  smfdiv  46718  smfsuplem1  46732  smfliminflem  46751  fmtno4prm  47449