Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  risset Structured version   Unicode version

Theorem risset 2745
 Description: Two ways to say " belongs to ." (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
risset
Distinct variable groups:   ,   ,

Proof of Theorem risset
StepHypRef Expression
1 exancom 1596 . 2
2 df-rex 2703 . 2
3 df-clel 2431 . 2
41, 2, 33bitr4ri 270 1
 Colors of variables: wff set class Syntax hints:   wb 177   wa 359  wex 1550   wceq 1652   wcel 1725  wrex 2698 This theorem is referenced by:  reueq  3123  reuind  3129  0el  3636  iunid  4138  sucel  4646  reusv3  4723  fvmptt  5812  releldm2  6389  qsid  6962  zorng  8376  rereccl  9724  nndiv  10032  zq  10572  4fvwrd4  11113  incexc2  12610  ruclem12  12832  conjnmzb  15032  pgpfac1lem2  15625  pgpfac1lem4  15628  fmid  17984  dcubic  20678  chscllem2  23132  ballotlemsima  24765  dfon2lem8  25409  brimg  25774  tfrqfree  25788  altopelaltxp  25813  prtlem9  26704  prtlem11  26706  prter2  26721  elnn0rabdioph  26854  fiphp3d  26871  phisum  27486  2llnmat  30258  2lnat  30518  cdlemefrs29bpre1  31131 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-clel 2431  df-rex 2703
 Copyright terms: Public domain W3C validator