MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elinel2 Structured version   Visualization version   GIF version

Theorem elinel2 4126
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
StepHypRef Expression
1 elin 3900 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21simprbi 500 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cin 3883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891
This theorem is referenced by:  elin2d  4129  eldmeldmressn  5866  onfr  6202  partfun  6471  fvcofneq  6840  offres  7670  fsplitfpar  7801  ressuppss  7836  wfrlem4  7945  smores3  7977  erdisj  8328  dffi2  8875  r0weon  9427  fodomfi2  9475  ackbij1lem6  9640  ackbij1lem9  9643  ackbij1lem10  9644  ackbij1lem11  9645  ackbij1lem18  9652  isfin1-3  9801  dedekindle  10797  uzdisj  12979  nn0disj  13022  rlimres  14911  lo1res  14912  ackbijnn  15179  bitsinv2  15786  bitsf1ocnv  15787  smueqlem  15833  prmrec  16252  isstruct2  16489  isacs2  16920  isdrs2  17545  isacs3lem  17772  subrgpropd  19567  sralmod  19956  basdif0  21562  clsval2  21659  mreclatdemoBAD  21705  restfpw  21788  fincmp  22002  discmp  22007  uncmp  22012  cmpfi  22017  bwth  22019  iunconn  22037  1stcrest  22062  infil  22472  alexsublem  22653  alexsubALTlem3  22658  tsmsfbas  22737  tsmsgsum  22748  tsmssubm  22752  tsmsres  22753  tsmsf1o  22754  tsmsmhm  22755  tsmsadd  22756  tsmsxplem1  22762  tsmsxp  22764  blres  23042  reconnlem2  23436  xrge0tsms  23443  ncvsge0  23762  cphsscph  23859  cfilres  23904  ioombl1lem4  24169  mbfadd  24269  mbfsub  24270  mbfmul  24334  itg2cnlem2  24370  bddmulibl  24446  ellimc2  24484  fsumvma2  25802  vmasum  25804  chpchtsum  25807  chebbnd1lem1  26057  dirith2  26116  uhgrspansubgrlem  27084  disjin2  30354  xrge0tsmsd  30746  prsdm  31271  prsrn  31272  frrlem4  33240  frrlem11  33247  frrlem12  33248  pibt2  34835  heicant  35091  mndoisexid  35306  eqvreldisj  36008  fiinfi  40265  restuni3  41746  nel2nelin  41777  disjinfi  41813  inmap  41831  iocopn  42150  icoopn  42155  icomnfinre  42182  uzinico  42190  islpcn  42274  lptre2pt  42275  limcresiooub  42277  limcresioolb  42278  limclner  42286  limsupmnflem  42355  limsupresxr  42401  liminfresxr  42402  liminfvalxr  42418  icccncfext  42522  stoweidlem39  42674  stoweidlem50  42685  stoweidlem57  42692  fourierdlem32  42774  fourierdlem33  42775  fourierdlem48  42789  fourierdlem49  42790  fourierdlem71  42812  fourierdlem80  42821  qndenserrnbllem  42929  sge0rnre  42996  sge0z  43007  sge0tsms  43012  sge0cl  43013  sge0f1o  43014  sge0fsum  43019  sge0sup  43023  sge0rnbnd  43025  sge0ltfirp  43032  sge0resplit  43038  sge0le  43039  sge0split  43041  sge0iunmptlemre  43047  sge0ltfirpmpt2  43058  sge0isum  43059  sge0xaddlem1  43065  sge0xaddlem2  43066  sge0pnffsumgt  43074  sge0gtfsumgt  43075  sge0uzfsumgt  43076  sge0seq  43078  sge0reuz  43079  meadjiunlem  43097  caragendifcl  43146  omeiunltfirp  43151  carageniuncllem2  43154  caratheodorylem2  43159  hspmbllem2  43259  pimiooltgt  43339  pimdecfgtioc  43343  pimincfltioc  43344  pimdecfgtioo  43345  pimincfltioo  43346  sssmf  43365  smfaddlem1  43389  smfaddlem2  43390  smfadd  43391  mbfpsssmf  43409  smfmullem4  43419  smfmul  43420  smfdiv  43422  smfsuplem1  43435  smfliminflem  43454  fmtno4prm  44085  rnghmsubcsetclem2  44593  rhmsubcsetclem2  44639  rhmsubcrngclem2  44645
  Copyright terms: Public domain W3C validator