Theorem elpri 4013

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	|- ( A e. { B , C } -> ( A = B \/ A = C ) )

Proof of Theorem elpri

Step	Hyp	Ref	Expression
1		elprg 4009	. 2 |- ( A e. { B , C } -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
2	1	ibi 244	1 |- ( A e. { B , C } -> ( A = B \/ A = C ) )

Syntax hints:   -> wi 4   \/ wo 369   = wceq 1437   e. wcel 1867   {cpr 3995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-un 3438  df-sn 3994  df-pr 3996

This theorem is referenced by:  nelpri  4014  nelprd  4015  tppreqb  4135  opth1  4686  0nelop  4702  funtpg  5642  ftpg  6080  2oconcl  7204  cantnflem2  8185  m1expcl2  12280  hash2prd  12616  hash2pwpr  12617  bitsinv1lem  14378  xpscfv  15420  xpsfeq  15422  pmtrprfval  17080  m1expaddsub  17091  psgnprfval  17114  frgpuptinv  17362  frgpup3lem  17368  cnmsgnsubg  19082  zrhpsgnelbas  19099  mdetralt  19570  m2detleiblem1  19586  indiscld  20044  cnindis  20245  conclo  20367  txindis  20586  xpsxmetlem  21331  xpsmet  21334  ishl2  22256  recnprss  22766  recnperf  22767  dvlip2  22854  coseq0negpitopi  23362  pythag  23650  reasinsin  23726  scvxcvx  23815  perfectlem2  24060  lgslem4  24129  lgseisenlem2  24180  usgraedg4  25001  cusgrares  25086  2pthlem2  25212  vdgr1a  25520  konigsberg  25601  ex-pr  25766  elpreq  28036  1neg1t1neg1  28209  signswch  29279  kur14lem7  29764  poimirlem31  31719  ftc1anclem2  31766  wepwsolem  35654  relexp01min  35992  ssrecnpr  36341  seff  36342  sblpnf  36343  expgrowthi  36367  dvconstbi  36368  sumpair  37044  refsum2cnlem1  37046  iooinlbub  37231  elprn1  37333  elprn2  37334  cncfiooicclem1  37391  dvmptconst  37405  dvmptidg  37407  dvmulcncf  37417  dvdivcncf  37419  elprneb  38159  perfectALTVlem2  38291  usgvincvad  38531  usgvincvadALT  38534  0dig2pr01  39239