Theorem elinel2 4177

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3925

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933

This theorem is referenced by:  elin2d  4180  nel2nelin  4183  eldmeldmressn  6012  onfr  6391  partfun  6685  fvcofneq  7083  offres  7982  fsplitfpar  8117  ressuppss  8182  frrlem4  8288  frrlem11  8295  frrlem12  8296  wfrlem4OLD  8326  smores3  8367  erdisj  8773  dffi2  9435  r0weon  10026  fodomfi2  10074  ackbij1lem6  10238  ackbij1lem9  10241  ackbij1lem10  10242  ackbij1lem11  10243  ackbij1lem18  10250  isfin1-3  10400  dedekindle  11399  uzdisj  13614  nn0disj  13661  rlimres  15574  lo1res  15575  ackbijnn  15844  bitsinv2  16462  bitsf1ocnv  16463  smueqlem  16509  prmrec  16942  isstruct2  17168  isacs2  17665  isdrs2  18318  isacs3lem  18552  subrngpropd  20528  subrgpropd  20568  rnghmsubcsetclem2  20592  rhmsubcsetclem2  20621  rhmsubcrngclem2  20627  sralmod  21145  basdif0  22891  clsval2  22988  mreclatdemoBAD  23034  restfpw  23117  fincmp  23331  discmp  23336  uncmp  23341  cmpfi  23346  bwth  23348  iunconn  23366  1stcrest  23391  infil  23801  alexsublem  23982  alexsubALTlem3  23987  tsmsfbas  24066  tsmsgsum  24077  tsmssubm  24081  tsmsres  24082  tsmsf1o  24083  tsmsmhm  24084  tsmsadd  24085  tsmsxplem1  24091  tsmsxp  24093  blres  24370  reconnlem2  24767  xrge0tsms  24774  ncvsge0  25105  cphsscph  25203  cfilres  25248  ioombl1lem4  25514  mbfadd  25614  mbfsub  25615  mbfmul  25679  itg2cnlem2  25715  bddmulibl  25792  ellimc2  25830  fsumvma2  27177  vmasum  27179  chpchtsum  27182  chebbnd1lem1  27432  dirith2  27491  uhgrspansubgrlem  29269  disjin2  32568  xrge0tsmsd  33056  prsdm  33945  prsrn  33946  pibt2  37435  heicant  37679  mndoisexid  37893  eqvreldisj  38632  fiinfi  43597  ismnushort  44325  restuni3  45142  disjinfi  45216  inmap  45233  iocopn  45549  icoopn  45554  icomnfinre  45581  uzinico  45588  islpcn  45668  lptre2pt  45669  limcresiooub  45671  limcresioolb  45672  limclner  45680  limsupmnflem  45749  limsupresxr  45795  liminfresxr  45796  liminfvalxr  45812  icccncfext  45916  stoweidlem39  46068  stoweidlem50  46079  stoweidlem57  46086  fourierdlem32  46168  fourierdlem33  46169  fourierdlem48  46183  fourierdlem49  46184  fourierdlem71  46206  fourierdlem80  46215  qndenserrnbllem  46323  sge0rnre  46393  sge0z  46404  sge0tsms  46409  sge0cl  46410  sge0f1o  46411  sge0fsum  46416  sge0sup  46420  sge0rnbnd  46422  sge0ltfirp  46429  sge0resplit  46435  sge0le  46436  sge0split  46438  sge0iunmptlemre  46444  sge0ltfirpmpt2  46455  sge0isum  46456  sge0xaddlem1  46462  sge0xaddlem2  46463  sge0pnffsumgt  46471  sge0gtfsumgt  46472  sge0uzfsumgt  46473  sge0seq  46475  sge0reuz  46476  meadjiunlem  46494  caragendifcl  46543  omeiunltfirp  46548  carageniuncllem2  46551  caratheodorylem2  46556  hspmbllem2  46656  pimiooltgt  46739  pimdecfgtioc  46744  pimincfltioc  46745  pimdecfgtioo  46746  pimincfltioo  46747  sssmf  46767  smfaddlem1  46792  smfaddlem2  46793  smfadd  46794  mbfpsssmf  46812  smfmullem4  46823  smfmul  46824  smfdiv  46826  smfsuplem1  46840  smfliminflem  46859  fmtno4prm  47589