Theorem elinel2 4176

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-in 3946

This theorem is referenced by:  elin2d  4179  eldmeldmressn  5899  onfr  6233  fvcofneq  6862  offres  7687  fsplitfpar  7817  ressuppss  7852  wfrlem4  7961  smores3  7993  erdisj  8344  dffi2  8890  r0weon  9441  fodomfi2  9489  ackbij1lem6  9650  ackbij1lem9  9653  ackbij1lem10  9654  ackbij1lem11  9655  ackbij1lem18  9662  isfin1-3  9811  dedekindle  10807  uzdisj  12983  nn0disj  13026  rlimres  14918  lo1res  14919  ackbijnn  15186  bitsinv2  15795  bitsf1ocnv  15796  smueqlem  15842  prmrec  16261  isstruct2  16496  isacs2  16927  isdrs2  17552  isacs3lem  17779  subrgpropd  19573  sralmod  19962  basdif0  21564  clsval2  21661  mreclatdemoBAD  21707  restfpw  21790  fincmp  22004  discmp  22009  uncmp  22014  cmpfi  22019  bwth  22021  iunconn  22039  1stcrest  22064  infil  22474  alexsublem  22655  alexsubALTlem3  22660  tsmsfbas  22739  tsmsgsum  22750  tsmssubm  22754  tsmsres  22755  tsmsf1o  22756  tsmsmhm  22757  tsmsadd  22758  tsmsxplem1  22764  tsmsxp  22766  blres  23044  reconnlem2  23438  xrge0tsms  23445  ncvsge0  23760  cphsscph  23857  cfilres  23902  ioombl1lem4  24165  mbfadd  24265  mbfsub  24266  mbfmul  24330  itg2cnlem2  24366  bddmulibl  24442  ellimc2  24478  fsumvma2  25793  vmasum  25795  chpchtsum  25798  chebbnd1lem1  26048  dirith2  26107  uhgrspansubgrlem  27075  disjin2  30340  partfun  30424  xrge0tsmsd  30696  prsdm  31161  prsrn  31162  frrlem4  33130  frrlem11  33137  frrlem12  33138  pibt2  34702  heicant  34931  mndoisexid  35151  eqvreldisj  35853  fiinfi  39938  restuni3  41390  nel2nelin  41422  disjinfi  41460  inmap  41478  iocopn  41802  icoopn  41807  icomnfinre  41834  uzinico  41842  islpcn  41926  lptre2pt  41927  limcresiooub  41929  limcresioolb  41930  limclner  41938  limsupmnflem  42007  limsupresxr  42053  liminfresxr  42054  liminfvalxr  42070  icccncfext  42176  stoweidlem39  42331  stoweidlem50  42342  stoweidlem57  42349  fourierdlem32  42431  fourierdlem33  42432  fourierdlem48  42446  fourierdlem49  42447  fourierdlem71  42469  fourierdlem80  42478  qndenserrnbllem  42586  sge0rnre  42653  sge0z  42664  sge0tsms  42669  sge0cl  42670  sge0f1o  42671  sge0fsum  42676  sge0sup  42680  sge0rnbnd  42682  sge0ltfirp  42689  sge0resplit  42695  sge0le  42696  sge0split  42698  sge0iunmptlemre  42704  sge0ltfirpmpt2  42715  sge0isum  42716  sge0xaddlem1  42722  sge0xaddlem2  42723  sge0pnffsumgt  42731  sge0gtfsumgt  42732  sge0uzfsumgt  42733  sge0seq  42735  sge0reuz  42736  meadjiunlem  42754  caragendifcl  42803  omeiunltfirp  42808  carageniuncllem2  42811  caratheodorylem2  42816  hspmbllem2  42916  pimiooltgt  42996  pimdecfgtioc  43000  pimincfltioc  43001  pimdecfgtioo  43002  pimincfltioo  43003  sssmf  43022  smfaddlem1  43046  smfaddlem2  43047  smfadd  43048  mbfpsssmf  43066  smfmullem4  43076  smfmul  43077  smfdiv  43079  smfsuplem1  43092  smfliminflem  43111  fmtno4prm  43744  rnghmsubcsetclem2  44254  rhmsubcsetclem2  44300  rhmsubcrngclem2  44306