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  37705  mndoisexid  37919  eqvreldisj  38720  fiinfi  43676  ismnushort  44404  restuni3  45225  disjinfi  45299  inmap  45316  iocopn  45630  icoopn  45635  icomnfinre  45662  uzinico  45669  islpcn  45747  lptre2pt  45748  limcresiooub  45750  limcresioolb  45751  limclner  45759  limsupmnflem  45828  limsupresxr  45874  liminfresxr  45875  liminfvalxr  45891  icccncfext  45995  stoweidlem39  46147  stoweidlem50  46158  stoweidlem57  46165  fourierdlem32  46247  fourierdlem33  46248  fourierdlem48  46262  fourierdlem49  46263  fourierdlem71  46285  fourierdlem80  46294  qndenserrnbllem  46402  sge0rnre  46472  sge0z  46483  sge0tsms  46488  sge0cl  46489  sge0f1o  46490  sge0fsum  46495  sge0sup  46499  sge0rnbnd  46501  sge0ltfirp  46508  sge0resplit  46514  sge0le  46515  sge0split  46517  sge0iunmptlemre  46523  sge0ltfirpmpt2  46534  sge0isum  46535  sge0xaddlem1  46541  sge0xaddlem2  46542  sge0pnffsumgt  46550  sge0gtfsumgt  46551  sge0uzfsumgt  46552  sge0seq  46554  sge0reuz  46555  meadjiunlem  46573  caragendifcl  46622  omeiunltfirp  46627  carageniuncllem2  46630  caratheodorylem2  46635  hspmbllem2  46735  pimiooltgt  46818  pimdecfgtioc  46823  pimincfltioc  46824  pimdecfgtioo  46825  pimincfltioo  46826  sssmf  46846  smfaddlem1  46871  smfaddlem2  46872  smfadd  46873  mbfpsssmf  46891  smfmullem4  46902  smfmul  46903  smfdiv  46905  smfsuplem1  46919  smfliminflem  46938  fmtno4prm  47685