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

Theorem risset 2982
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 1671 . 2
2 df-rex 2813 . 2
3 df-clel 2452 . 2
41, 2, 33bitr4ri 278 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  reueq  3297  reuind  3303  0el  3802  iunid  4385  reusv3  4660  sucel  4956  fvmptt  5971  releldm2  6850  qsid  7396  zorng  8905  rereccl  10287  nndiv  10601  zq  11217  4fvwrd4  11822  wrdlen1  12579  incexc2  13650  ruclem12  13974  conjnmzb  16301  symgmov1  16417  pgpfac1lem2  17126  pgpfac1lem4  17129  mat1dimelbas  18973  mat1dimbas  18974  chmaidscmat  19349  unisngl  20028  fmid  20461  dcubic  23177  usgn0fidegnn0  25029  chscllem2  26556  disjunsn  27453  ballotlemsima  28454  dfon2lem8  29222  brimg  29587  tfrqfree  29601  altopelaltxp  29626  prtlem9  30605  prtlem11  30607  prter2  30622  elnn0rabdioph  30736  fiphp3d  30753  phisum  31159  2llnmat  35248  2lnat  35508  cdlemefrs29bpre1  36123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-clel 2452  df-rex 2813
  Copyright terms: Public domain W3C validator