Theorem elinel2 3800

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
elinel2	|- ( A e. ( B i^i C ) -> A e. C )

Proof of Theorem elinel2

Step	Hyp	Ref	Expression
1		elin 3796	. 2 |- ( A e. ( B i^i C ) <-> ( A e. B /\ A e. C ) )
2	1	simprbi 480	1 |- ( A e. ( B i^i C ) -> A e. C )

Syntax hints:   -> wi 4   e. wcel 1990   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  elin2d  3803  eldmeldmressn  5440  onfr  5763  ncvsge0  22953  itg2cnlem2  23529  uhgrspansubgrlem  26182  disjin2  29400  partfun  29475  xrge0tsmsd  29785  heicant  33444  mndoisexid  33668  fiinfi  37878  restuni3  39301  nel2nelin  39338  disjinfi  39380  inmap  39401  iocopn  39746  icoopn  39751  icomnfinre  39779  uzinico  39787  islpcn  39871  lptre2pt  39872  limcresiooub  39874  limcresioolb  39875  limclner  39883  limsupmnflem  39952  limsupresxr  39998  liminfresxr  39999  liminfvalxr  40015  icccncfext  40100  stoweidlem39  40256  stoweidlem50  40267  stoweidlem57  40274  fourierdlem32  40356  fourierdlem33  40357  fourierdlem48  40371  fourierdlem49  40372  fourierdlem71  40394  fourierdlem80  40403  qndenserrnbllem  40514  sge0rnre  40581  sge0z  40592  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0fsum  40604  sge0sup  40608  sge0rnbnd  40610  sge0ltfirp  40617  sge0resplit  40623  sge0le  40624  sge0split  40626  sge0iunmptlemre  40632  sge0ltfirpmpt2  40643  sge0isum  40644  sge0xaddlem1  40650  sge0xaddlem2  40651  sge0pnffsumgt  40659  sge0gtfsumgt  40660  sge0uzfsumgt  40661  sge0seq  40663  sge0reuz  40664  meadjiunlem  40682  caragendifcl  40728  omeiunltfirp  40733  carageniuncllem2  40736  caratheodorylem2  40741  hspmbllem2  40841  pimiooltgt  40921  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  sssmf  40947  smfaddlem1  40971  smfaddlem2  40972  smfadd  40973  mbfpsssmf  40991  smfmullem4  41001  smfmul  41002  smfdiv  41004  smfsuplem1  41017  smfliminflem  41036  fmtno4prm  41487  rnghmsubcsetclem2  41976  rhmsubcsetclem2  42022  rhmsubcrngclem2  42028