Theorem elpri 4047

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

Syntax hints:   -> wi 4   \/ wo 368   = wceq 1379   e. wcel 1767   {cpr 4029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030

This theorem is referenced by:  nelpri  4048  nelprd  4049  tppreqb  4168  opth1  4720  0nelop  4737  funtpg  5638  ftpg  6071  2oconcl  7153  cantnflem2  8109  m1expcl2  12156  hash2prd  12484  hash2pwpr  12485  bitsinv1lem  13950  xpscfv  14817  xpsfeq  14819  pmtrprfval  16318  m1expaddsub  16329  psgnprfval  16352  frgpuptinv  16595  frgpup3lem  16601  cnmsgnsubg  18408  zrhpsgnelbas  18425  mdetralt  18905  m2detleiblem1  18921  indiscld  19386  cnindis  19587  conclo  19710  txindis  19898  xpsxmetlem  20645  xpsmet  20648  ishl2  21573  recnprss  22071  recnperf  22072  dvlip2  22159  coseq0negpitopi  22657  pythag  22905  reasinsin  22983  scvxcvx  23071  perfectlem2  23261  lgslem4  23330  lgseisenlem2  23381  usgraedg4  24091  cusgrares  24176  2pthlem2  24302  vdgr1a  24610  konigsberg  24691  ex-pr  24856  elpreq  27119  signswch  28186  kur14lem7  28324  ftc1anclem2  29696  wepwsolem  30619  ssrecnpr  30819  seff  30820  sblpnf  30821  expgrowthi  30866  dvconstbi  30867  sumpair  31016  refsum2cnlem1  31018  iooinlbub  31126  cncfiooicclem1  31260  dvmptconst  31271  dvmptidg  31273  dvmulcncf  31283  dvdivcncf  31285  usgvincvad  31899  usgvincvadALT  31902