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

Theorem risset 2603
 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 1576 . 2
2 df-rex 2562 . 2
3 df-clel 2292 . 2
41, 2, 33bitr4ri 269 1
 Colors of variables: wff set class Syntax hints:   wb 176   wa 358  wex 1531   wceq 1632   wcel 1696  wrex 2557 This theorem is referenced by:  reueq  2975  reuind  2981  0el  3484  iunid  3973  sucel  4481  reusv3  4558  fvmptt  5631  releldm2  6186  qsid  6741  zorng  8147  rereccl  9494  nndiv  9802  zq  10338  incexc2  12313  ruclem12  12535  conjnmzb  14733  pgpfac1lem2  15326  pgpfac1lem4  15329  fmid  17671  dcubic  20158  chscllem2  22233  ballotlemsima  23090  dfon2lem8  24217  elfuns  24525  tfrqfree  24561  altopelaltxp  24582  bsstrs  26249  nbssntrs  26250  prtlem9  26835  prtlem11  26837  prter2  26852  elnn0rabdioph  26987  fiphp3d  27005  phisum  27621  4fvwrd4  28220  2llnmat  30335  2lnat  30595  cdlemefrs29bpre1  31208 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-clel 2292  df-rex 2562
 Copyright terms: Public domain W3C validator