Theorem elinel2 4161

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

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

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 3446  df-in 3918

This theorem is referenced by:  elin2d  4164  nel2nelin  4167  eldmeldmressn  5985  onfr  6359  partfun  6647  fvcofneq  7047  offres  7941  fsplitfpar  8074  ressuppss  8139  frrlem4  8245  frrlem11  8252  frrlem12  8253  smores3  8299  erdisj  8705  dffi2  9350  r0weon  9941  fodomfi2  9989  ackbij1lem6  10153  ackbij1lem9  10156  ackbij1lem10  10157  ackbij1lem11  10158  ackbij1lem18  10165  isfin1-3  10315  dedekindle  11314  uzdisj  13534  nn0disj  13581  rlimres  15500  lo1res  15501  ackbijnn  15770  bitsinv2  16389  bitsf1ocnv  16390  smueqlem  16436  prmrec  16869  isstruct2  17095  isacs2  17594  isdrs2  18247  isacs3lem  18483  subrngpropd  20488  subrgpropd  20528  rnghmsubcsetclem2  20552  rhmsubcsetclem2  20581  rhmsubcrngclem2  20587  sralmod  21126  basdif0  22873  clsval2  22970  mreclatdemoBAD  23016  restfpw  23099  fincmp  23313  discmp  23318  uncmp  23323  cmpfi  23328  bwth  23330  iunconn  23348  1stcrest  23373  infil  23783  alexsublem  23964  alexsubALTlem3  23969  tsmsfbas  24048  tsmsgsum  24059  tsmssubm  24063  tsmsres  24064  tsmsf1o  24065  tsmsmhm  24066  tsmsadd  24067  tsmsxplem1  24073  tsmsxp  24075  blres  24352  reconnlem2  24749  xrge0tsms  24756  ncvsge0  25086  cphsscph  25184  cfilres  25229  ioombl1lem4  25495  mbfadd  25595  mbfsub  25596  mbfmul  25660  itg2cnlem2  25696  bddmulibl  25773  ellimc2  25811  fsumvma2  27158  vmasum  27160  chpchtsum  27163  chebbnd1lem1  27413  dirith2  27472  uhgrspansubgrlem  29270  disjin2  32566  xrge0tsmsd  33045  prsdm  33897  prsrn  33898  pibt2  37398  heicant  37642  mndoisexid  37856  eqvreldisj  38598  fiinfi  43555  ismnushort  44283  restuni3  45105  disjinfi  45179  inmap  45196  iocopn  45511  icoopn  45516  icomnfinre  45543  uzinico  45550  islpcn  45630  lptre2pt  45631  limcresiooub  45633  limcresioolb  45634  limclner  45642  limsupmnflem  45711  limsupresxr  45757  liminfresxr  45758  liminfvalxr  45774  icccncfext  45878  stoweidlem39  46030  stoweidlem50  46041  stoweidlem57  46048  fourierdlem32  46130  fourierdlem33  46131  fourierdlem48  46145  fourierdlem49  46146  fourierdlem71  46168  fourierdlem80  46177  qndenserrnbllem  46285  sge0rnre  46355  sge0z  46366  sge0tsms  46371  sge0cl  46372  sge0f1o  46373  sge0fsum  46378  sge0sup  46382  sge0rnbnd  46384  sge0ltfirp  46391  sge0resplit  46397  sge0le  46398  sge0split  46400  sge0iunmptlemre  46406  sge0ltfirpmpt2  46417  sge0isum  46418  sge0xaddlem1  46424  sge0xaddlem2  46425  sge0pnffsumgt  46433  sge0gtfsumgt  46434  sge0uzfsumgt  46435  sge0seq  46437  sge0reuz  46438  meadjiunlem  46456  caragendifcl  46505  omeiunltfirp  46510  carageniuncllem2  46513  caratheodorylem2  46518  hspmbllem2  46618  pimiooltgt  46701  pimdecfgtioc  46706  pimincfltioc  46707  pimdecfgtioo  46708  pimincfltioo  46709  sssmf  46729  smfaddlem1  46754  smfaddlem2  46755  smfadd  46756  mbfpsssmf  46774  smfmullem4  46785  smfmul  46786  smfdiv  46788  smfsuplem1  46802  smfliminflem  46821  fmtno4prm  47569