Theorem elinel2 4149

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  elin2d  4152  nel2nelin  4155  eldmeldmressn  5973  onfr  6345  partfun  6628  fvcofneq  7026  offres  7915  fsplitfpar  8048  ressuppss  8113  frrlem4  8219  frrlem11  8226  frrlem12  8227  smores3  8273  erdisj  8679  dffi2  9307  r0weon  9903  fodomfi2  9951  ackbij1lem6  10115  ackbij1lem9  10118  ackbij1lem10  10119  ackbij1lem11  10120  ackbij1lem18  10127  isfin1-3  10277  dedekindle  11277  uzdisj  13497  nn0disj  13544  rlimres  15465  lo1res  15466  ackbijnn  15735  bitsinv2  16354  bitsf1ocnv  16355  smueqlem  16401  prmrec  16834  isstruct2  17060  isacs2  17559  isdrs2  18212  isacs3lem  18448  subrngpropd  20483  subrgpropd  20523  rnghmsubcsetclem2  20547  rhmsubcsetclem2  20576  rhmsubcrngclem2  20582  sralmod  21121  basdif0  22868  clsval2  22965  mreclatdemoBAD  23011  restfpw  23094  fincmp  23308  discmp  23313  uncmp  23318  cmpfi  23323  bwth  23325  iunconn  23343  1stcrest  23368  infil  23778  alexsublem  23959  alexsubALTlem3  23964  tsmsfbas  24043  tsmsgsum  24054  tsmssubm  24058  tsmsres  24059  tsmsf1o  24060  tsmsmhm  24061  tsmsadd  24062  tsmsxplem1  24068  tsmsxp  24070  blres  24346  reconnlem2  24743  xrge0tsms  24750  ncvsge0  25080  cphsscph  25178  cfilres  25223  ioombl1lem4  25489  mbfadd  25589  mbfsub  25590  mbfmul  25654  itg2cnlem2  25690  bddmulibl  25767  ellimc2  25805  fsumvma2  27152  vmasum  27154  chpchtsum  27157  chebbnd1lem1  27407  dirith2  27466  uhgrspansubgrlem  29268  disjin2  32567  xrge0tsmsd  33042  prsdm  33927  prsrn  33928  pibt2  37461  heicant  37694  mndoisexid  37908  eqvreldisj  38709  fiinfi  43665  ismnushort  44393  restuni3  45214  disjinfi  45288  inmap  45305  iocopn  45619  icoopn  45624  icomnfinre  45651  uzinico  45658  islpcn  45736  lptre2pt  45737  limcresiooub  45739  limcresioolb  45740  limclner  45748  limsupmnflem  45817  limsupresxr  45863  liminfresxr  45864  liminfvalxr  45880  icccncfext  45984  stoweidlem39  46136  stoweidlem50  46147  stoweidlem57  46154  fourierdlem32  46236  fourierdlem33  46237  fourierdlem48  46251  fourierdlem49  46252  fourierdlem71  46274  fourierdlem80  46283  qndenserrnbllem  46391  sge0rnre  46461  sge0z  46472  sge0tsms  46477  sge0cl  46478  sge0f1o  46479  sge0fsum  46484  sge0sup  46488  sge0rnbnd  46490  sge0ltfirp  46497  sge0resplit  46503  sge0le  46504  sge0split  46506  sge0iunmptlemre  46512  sge0ltfirpmpt2  46523  sge0isum  46524  sge0xaddlem1  46530  sge0xaddlem2  46531  sge0pnffsumgt  46539  sge0gtfsumgt  46540  sge0uzfsumgt  46541  sge0seq  46543  sge0reuz  46544  meadjiunlem  46562  caragendifcl  46611  omeiunltfirp  46616  carageniuncllem2  46619  caratheodorylem2  46624  hspmbllem2  46724  pimiooltgt  46807  pimdecfgtioc  46812  pimincfltioc  46813  pimdecfgtioo  46814  pimincfltioo  46815  sssmf  46835  smfaddlem1  46860  smfaddlem2  46861  smfadd  46862  mbfpsssmf  46880  smfmullem4  46891  smfmul  46892  smfdiv  46894  smfsuplem1  46908  smfliminflem  46927  fmtno4prm  47674