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

Theorem elinel2 4157
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 3927 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21simprbi 498 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cin 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918
This theorem is referenced by:  elin2d  4160  eldmeldmressn  5982  onfr  6357  partfun  6649  fvcofneq  7044  offres  7917  fsplitfpar  8051  ressuppss  8115  frrlem4  8221  frrlem11  8228  frrlem12  8229  wfrlem4OLD  8259  smores3  8300  erdisj  8701  dffi2  9360  r0weon  9949  fodomfi2  9997  ackbij1lem6  10162  ackbij1lem9  10165  ackbij1lem10  10166  ackbij1lem11  10167  ackbij1lem18  10174  isfin1-3  10323  dedekindle  11320  uzdisj  13515  nn0disj  13558  rlimres  15441  lo1res  15442  ackbijnn  15714  bitsinv2  16324  bitsf1ocnv  16325  smueqlem  16371  prmrec  16795  isstruct2  17022  isacs2  17534  isdrs2  18196  isacs3lem  18432  subrgpropd  20260  sralmod  20659  basdif0  22306  clsval2  22404  mreclatdemoBAD  22450  restfpw  22533  fincmp  22747  discmp  22752  uncmp  22757  cmpfi  22762  bwth  22764  iunconn  22782  1stcrest  22807  infil  23217  alexsublem  23398  alexsubALTlem3  23403  tsmsfbas  23482  tsmsgsum  23493  tsmssubm  23497  tsmsres  23498  tsmsf1o  23499  tsmsmhm  23500  tsmsadd  23501  tsmsxplem1  23507  tsmsxp  23509  blres  23787  reconnlem2  24193  xrge0tsms  24200  ncvsge0  24520  cphsscph  24618  cfilres  24663  ioombl1lem4  24928  mbfadd  25028  mbfsub  25029  mbfmul  25094  itg2cnlem2  25130  bddmulibl  25206  ellimc2  25244  fsumvma2  26565  vmasum  26567  chpchtsum  26570  chebbnd1lem1  26820  dirith2  26879  uhgrspansubgrlem  28241  disjin2  31508  xrge0tsmsd  31902  prsdm  32498  prsrn  32499  pibt2  35891  heicant  36116  mndoisexid  36331  eqvreldisj  37079  fiinfi  41852  ismnushort  42588  restuni3  43335  nel2nelin  43364  disjinfi  43419  inmap  43437  iocopn  43765  icoopn  43770  icomnfinre  43797  uzinico  43805  islpcn  43887  lptre2pt  43888  limcresiooub  43890  limcresioolb  43891  limclner  43899  limsupmnflem  43968  limsupresxr  44014  liminfresxr  44015  liminfvalxr  44031  icccncfext  44135  stoweidlem39  44287  stoweidlem50  44298  stoweidlem57  44305  fourierdlem32  44387  fourierdlem33  44388  fourierdlem48  44402  fourierdlem49  44403  fourierdlem71  44425  fourierdlem80  44434  qndenserrnbllem  44542  sge0rnre  44612  sge0z  44623  sge0tsms  44628  sge0cl  44629  sge0f1o  44630  sge0fsum  44635  sge0sup  44639  sge0rnbnd  44641  sge0ltfirp  44648  sge0resplit  44654  sge0le  44655  sge0split  44657  sge0iunmptlemre  44663  sge0ltfirpmpt2  44674  sge0isum  44675  sge0xaddlem1  44681  sge0xaddlem2  44682  sge0pnffsumgt  44690  sge0gtfsumgt  44691  sge0uzfsumgt  44692  sge0seq  44694  sge0reuz  44695  meadjiunlem  44713  caragendifcl  44762  omeiunltfirp  44767  carageniuncllem2  44770  caratheodorylem2  44775  hspmbllem2  44875  pimiooltgt  44958  pimdecfgtioc  44963  pimincfltioc  44964  pimdecfgtioo  44965  pimincfltioo  44966  sssmf  44986  smfaddlem1  45011  smfaddlem2  45012  smfadd  45013  mbfpsssmf  45031  smfmullem4  45042  smfmul  45043  smfdiv  45045  smfsuplem1  45059  smfliminflem  45078  fmtno4prm  45774  rnghmsubcsetclem2  46281  rhmsubcsetclem2  46327  rhmsubcrngclem2  46333
  Copyright terms: Public domain W3C validator