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

Theorem elpri 3826
 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 3823 . 2
21ibi 233 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 358   wceq 1652   wcel 1725  cpr 3807 This theorem is referenced by:  nelpri  3827  tppreqb  3931  opth1  4426  0nelop  4438  funtpg  5493  ftpg  5908  2oconcl  6739  cantnflem2  7636  m1expcl2  11393  bitsinv1lem  12943  xpscfv  13777  xpsfeq  13779  frgpuptinv  15393  frgpup3lem  15399  indiscld  17145  cnindis  17346  conclo  17468  txindis  17656  xpsxmetlem  18399  xpsmet  18402  ishl2  19314  recnprss  19781  recnperf  19782  dvlip2  19869  coseq0negpitopi  20401  pythag  20649  reasinsin  20726  scvxcvx  20814  perfectlem2  21004  lgslem4  21073  lgseisenlem2  21124  usgraedg4  21396  cusgrares  21471  2pthlem2  21586  vdgr1a  21667  konigsberg  21699  ex-pr  21728  elpreq  23989  kur14lem7  24888  wepwsolem  27070  m1expaddsub  27353  cnmsgnsubg  27366  ssrecnpr  27469  seff  27470  sblpnf  27471  expgrowthi  27482  dvconstbi  27483  sumpair  27637  refsum2cnlem1  27639  nelprd  28009 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-sn 3812  df-pr 3813
 Copyright terms: Public domain W3C validator