Theorem elinel2 4168

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924

This theorem is referenced by:  elin2d  4171  nel2nelin  4174  eldmeldmressn  5999  onfr  6374  partfun  6668  fvcofneq  7068  offres  7965  fsplitfpar  8100  ressuppss  8165  frrlem4  8271  frrlem11  8278  frrlem12  8279  smores3  8325  erdisj  8731  dffi2  9381  r0weon  9972  fodomfi2  10020  ackbij1lem6  10184  ackbij1lem9  10187  ackbij1lem10  10188  ackbij1lem11  10189  ackbij1lem18  10196  isfin1-3  10346  dedekindle  11345  uzdisj  13565  nn0disj  13612  rlimres  15531  lo1res  15532  ackbijnn  15801  bitsinv2  16420  bitsf1ocnv  16421  smueqlem  16467  prmrec  16900  isstruct2  17126  isacs2  17621  isdrs2  18274  isacs3lem  18508  subrngpropd  20484  subrgpropd  20524  rnghmsubcsetclem2  20548  rhmsubcsetclem2  20577  rhmsubcrngclem2  20583  sralmod  21101  basdif0  22847  clsval2  22944  mreclatdemoBAD  22990  restfpw  23073  fincmp  23287  discmp  23292  uncmp  23297  cmpfi  23302  bwth  23304  iunconn  23322  1stcrest  23347  infil  23757  alexsublem  23938  alexsubALTlem3  23943  tsmsfbas  24022  tsmsgsum  24033  tsmssubm  24037  tsmsres  24038  tsmsf1o  24039  tsmsmhm  24040  tsmsadd  24041  tsmsxplem1  24047  tsmsxp  24049  blres  24326  reconnlem2  24723  xrge0tsms  24730  ncvsge0  25060  cphsscph  25158  cfilres  25203  ioombl1lem4  25469  mbfadd  25569  mbfsub  25570  mbfmul  25634  itg2cnlem2  25670  bddmulibl  25747  ellimc2  25785  fsumvma2  27132  vmasum  27134  chpchtsum  27137  chebbnd1lem1  27387  dirith2  27446  uhgrspansubgrlem  29224  disjin2  32523  xrge0tsmsd  33009  prsdm  33911  prsrn  33912  pibt2  37412  heicant  37656  mndoisexid  37870  eqvreldisj  38612  fiinfi  43569  ismnushort  44297  restuni3  45119  disjinfi  45193  inmap  45210  iocopn  45525  icoopn  45530  icomnfinre  45557  uzinico  45564  islpcn  45644  lptre2pt  45645  limcresiooub  45647  limcresioolb  45648  limclner  45656  limsupmnflem  45725  limsupresxr  45771  liminfresxr  45772  liminfvalxr  45788  icccncfext  45892  stoweidlem39  46044  stoweidlem50  46055  stoweidlem57  46062  fourierdlem32  46144  fourierdlem33  46145  fourierdlem48  46159  fourierdlem49  46160  fourierdlem71  46182  fourierdlem80  46191  qndenserrnbllem  46299  sge0rnre  46369  sge0z  46380  sge0tsms  46385  sge0cl  46386  sge0f1o  46387  sge0fsum  46392  sge0sup  46396  sge0rnbnd  46398  sge0ltfirp  46405  sge0resplit  46411  sge0le  46412  sge0split  46414  sge0iunmptlemre  46420  sge0ltfirpmpt2  46431  sge0isum  46432  sge0xaddlem1  46438  sge0xaddlem2  46439  sge0pnffsumgt  46447  sge0gtfsumgt  46448  sge0uzfsumgt  46449  sge0seq  46451  sge0reuz  46452  meadjiunlem  46470  caragendifcl  46519  omeiunltfirp  46524  carageniuncllem2  46527  caratheodorylem2  46532  hspmbllem2  46632  pimiooltgt  46715  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  sssmf  46743  smfaddlem1  46768  smfaddlem2  46769  smfadd  46770  mbfpsssmf  46788  smfmullem4  46799  smfmul  46800  smfdiv  46802  smfsuplem1  46816  smfliminflem  46835  fmtno4prm  47580