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

Theorem elpri 4049
Description: If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.)
Assertion
Ref Expression
elpri

Proof of Theorem elpri
StepHypRef Expression
1 elprg 4045 . 2
21ibi 241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368  =wceq 1395  e.wcel 1818  {cpr 4031
This theorem is referenced by:  nelpri  4050  nelprd  4051  tppreqb  4171  opth1  4725  0nelop  4742  funtpg  5643  ftpg  6081  2oconcl  7172  cantnflem2  8130  m1expcl2  12188  hash2prd  12518  hash2pwpr  12519  bitsinv1lem  14091  xpscfv  14959  xpsfeq  14961  pmtrprfval  16512  m1expaddsub  16523  psgnprfval  16546  frgpuptinv  16789  frgpup3lem  16795  cnmsgnsubg  18613  zrhpsgnelbas  18630  mdetralt  19110  m2detleiblem1  19126  indiscld  19592  cnindis  19793  conclo  19916  txindis  20135  xpsxmetlem  20882  xpsmet  20885  ishl2  21810  recnprss  22308  recnperf  22309  dvlip2  22396  coseq0negpitopi  22896  pythag  23149  reasinsin  23227  scvxcvx  23315  perfectlem2  23505  lgslem4  23574  lgseisenlem2  23625  usgraedg4  24387  cusgrares  24472  2pthlem2  24598  vdgr1a  24906  konigsberg  24987  ex-pr  25151  elpreq  27417  signswch  28518  kur14lem7  28656  ftc1anclem2  30091  wepwsolem  30987  ssrecnpr  31188  seff  31189  sblpnf  31190  expgrowthi  31238  dvconstbi  31239  sumpair  31410  refsum2cnlem1  31412  iooinlbub  31534  elprn1  31639  elprn2  31640  cncfiooicclem1  31696  dvmptconst  31710  dvmptidg  31712  dvmulcncf  31722  dvdivcncf  31724  usgvincvad  32404  usgvincvadALT  32407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032
  Copyright terms: Public domain W3C validator