Theorem elinel2 4153

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

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

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 3438  df-in 3910

This theorem is referenced by:  elin2d  4156  nel2nelin  4159  eldmeldmressn  5976  onfr  6346  partfun  6629  fvcofneq  7027  offres  7918  fsplitfpar  8051  ressuppss  8116  frrlem4  8222  frrlem11  8229  frrlem12  8230  smores3  8276  erdisj  8682  dffi2  9313  r0weon  9906  fodomfi2  9954  ackbij1lem6  10118  ackbij1lem9  10121  ackbij1lem10  10122  ackbij1lem11  10123  ackbij1lem18  10130  isfin1-3  10280  dedekindle  11280  uzdisj  13500  nn0disj  13547  rlimres  15465  lo1res  15466  ackbijnn  15735  bitsinv2  16354  bitsf1ocnv  16355  smueqlem  16401  prmrec  16834  isstruct2  17060  isacs2  17559  isdrs2  18212  isacs3lem  18448  subrngpropd  20453  subrgpropd  20493  rnghmsubcsetclem2  20517  rhmsubcsetclem2  20546  rhmsubcrngclem2  20552  sralmod  21091  basdif0  22838  clsval2  22935  mreclatdemoBAD  22981  restfpw  23064  fincmp  23278  discmp  23283  uncmp  23288  cmpfi  23293  bwth  23295  iunconn  23313  1stcrest  23338  infil  23748  alexsublem  23929  alexsubALTlem3  23934  tsmsfbas  24013  tsmsgsum  24024  tsmssubm  24028  tsmsres  24029  tsmsf1o  24030  tsmsmhm  24031  tsmsadd  24032  tsmsxplem1  24038  tsmsxp  24040  blres  24317  reconnlem2  24714  xrge0tsms  24721  ncvsge0  25051  cphsscph  25149  cfilres  25194  ioombl1lem4  25460  mbfadd  25560  mbfsub  25561  mbfmul  25625  itg2cnlem2  25661  bddmulibl  25738  ellimc2  25776  fsumvma2  27123  vmasum  27125  chpchtsum  27128  chebbnd1lem1  27378  dirith2  27437  uhgrspansubgrlem  29235  disjin2  32531  xrge0tsmsd  33016  prsdm  33887  prsrn  33888  pibt2  37401  heicant  37645  mndoisexid  37859  eqvreldisj  38601  fiinfi  43556  ismnushort  44284  restuni3  45106  disjinfi  45180  inmap  45197  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