Theorem elinel2 4165

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3913

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921

This theorem is referenced by:  elin2d  4168  nel2nelin  4171  eldmeldmressn  5996  onfr  6371  partfun  6665  fvcofneq  7065  offres  7962  fsplitfpar  8097  ressuppss  8162  frrlem4  8268  frrlem11  8275  frrlem12  8276  smores3  8322  erdisj  8728  dffi2  9374  r0weon  9965  fodomfi2  10013  ackbij1lem6  10177  ackbij1lem9  10180  ackbij1lem10  10181  ackbij1lem11  10182  ackbij1lem18  10189  isfin1-3  10339  dedekindle  11338  uzdisj  13558  nn0disj  13605  rlimres  15524  lo1res  15525  ackbijnn  15794  bitsinv2  16413  bitsf1ocnv  16414  smueqlem  16460  prmrec  16893  isstruct2  17119  isacs2  17614  isdrs2  18267  isacs3lem  18501  subrngpropd  20477  subrgpropd  20517  rnghmsubcsetclem2  20541  rhmsubcsetclem2  20570  rhmsubcrngclem2  20576  sralmod  21094  basdif0  22840  clsval2  22937  mreclatdemoBAD  22983  restfpw  23066  fincmp  23280  discmp  23285  uncmp  23290  cmpfi  23295  bwth  23297  iunconn  23315  1stcrest  23340  infil  23750  alexsublem  23931  alexsubALTlem3  23936  tsmsfbas  24015  tsmsgsum  24026  tsmssubm  24030  tsmsres  24031  tsmsf1o  24032  tsmsmhm  24033  tsmsadd  24034  tsmsxplem1  24040  tsmsxp  24042  blres  24319  reconnlem2  24716  xrge0tsms  24723  ncvsge0  25053  cphsscph  25151  cfilres  25196  ioombl1lem4  25462  mbfadd  25562  mbfsub  25563  mbfmul  25627  itg2cnlem2  25663  bddmulibl  25740  ellimc2  25778  fsumvma2  27125  vmasum  27127  chpchtsum  27130  chebbnd1lem1  27380  dirith2  27439  uhgrspansubgrlem  29217  disjin2  32516  xrge0tsmsd  33002  prsdm  33904  prsrn  33905  pibt2  37405  heicant  37649  mndoisexid  37863  eqvreldisj  38605  fiinfi  43562  ismnushort  44290  restuni3  45112  disjinfi  45186  inmap  45203  iocopn  45518  icoopn  45523  icomnfinre  45550  uzinico  45557  islpcn  45637  lptre2pt  45638  limcresiooub  45640  limcresioolb  45641  limclner  45649  limsupmnflem  45718  limsupresxr  45764  liminfresxr  45765  liminfvalxr  45781  icccncfext  45885  stoweidlem39  46037  stoweidlem50  46048  stoweidlem57  46055  fourierdlem32  46137  fourierdlem33  46138  fourierdlem48  46152  fourierdlem49  46153  fourierdlem71  46175  fourierdlem80  46184  qndenserrnbllem  46292  sge0rnre  46362  sge0z  46373  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0fsum  46385  sge0sup  46389  sge0rnbnd  46391  sge0ltfirp  46398  sge0resplit  46404  sge0le  46405  sge0split  46407  sge0iunmptlemre  46413  sge0ltfirpmpt2  46424  sge0isum  46425  sge0xaddlem1  46431  sge0xaddlem2  46432  sge0pnffsumgt  46440  sge0gtfsumgt  46441  sge0uzfsumgt  46442  sge0seq  46444  sge0reuz  46445  meadjiunlem  46463  caragendifcl  46512  omeiunltfirp  46517  carageniuncllem2  46520  caratheodorylem2  46525  hspmbllem2  46625  pimiooltgt  46708  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  sssmf  46736  smfaddlem1  46761  smfaddlem2  46762  smfadd  46763  mbfpsssmf  46781  smfmullem4  46792  smfmul  46793  smfdiv  46795  smfsuplem1  46809  smfliminflem  46828  fmtno4prm  47576