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

Theorem elinel2 3943
 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 3939 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵𝐴𝐶))
21simprbi 483 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2139   ∩ cin 3714 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722 This theorem is referenced by:  elin2d  3946  eldmeldmressn  5598  onfr  5924  ncvsge0  23153  itg2cnlem2  23728  uhgrspansubgrlem  26381  disjin2  29707  partfun  29784  xrge0tsmsd  30094  frrlem4  32089  heicant  33757  mndoisexid  33981  fiinfi  38380  restuni3  39800  nel2nelin  39837  disjinfi  39879  inmap  39900  iocopn  40249  icoopn  40254  icomnfinre  40282  uzinico  40290  islpcn  40374  lptre2pt  40375  limcresiooub  40377  limcresioolb  40378  limclner  40386  limsupmnflem  40455  limsupresxr  40501  liminfresxr  40502  liminfvalxr  40518  icccncfext  40603  stoweidlem39  40759  stoweidlem50  40770  stoweidlem57  40777  fourierdlem32  40859  fourierdlem33  40860  fourierdlem48  40874  fourierdlem49  40875  fourierdlem71  40897  fourierdlem80  40906  qndenserrnbllem  41017  sge0rnre  41084  sge0z  41095  sge0tsms  41100  sge0cl  41101  sge0f1o  41102  sge0fsum  41107  sge0sup  41111  sge0rnbnd  41113  sge0ltfirp  41120  sge0resplit  41126  sge0le  41127  sge0split  41129  sge0iunmptlemre  41135  sge0ltfirpmpt2  41146  sge0isum  41147  sge0xaddlem1  41153  sge0xaddlem2  41154  sge0pnffsumgt  41162  sge0gtfsumgt  41163  sge0uzfsumgt  41164  sge0seq  41166  sge0reuz  41167  meadjiunlem  41185  caragendifcl  41234  omeiunltfirp  41239  carageniuncllem2  41242  caratheodorylem2  41247  hspmbllem2  41347  pimiooltgt  41427  pimdecfgtioc  41431  pimincfltioc  41432  pimdecfgtioo  41433  pimincfltioo  41434  sssmf  41453  smfaddlem1  41477  smfaddlem2  41478  smfadd  41479  mbfpsssmf  41497  smfmullem4  41507  smfmul  41508  smfdiv  41510  smfsuplem1  41523  smfliminflem  41542  fmtno4prm  41997  rnghmsubcsetclem2  42486  rhmsubcsetclem2  42532  rhmsubcrngclem2  42538
 Copyright terms: Public domain W3C validator