Theorem elpri 4197

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

Syntax hints:   -> wi 4   \/ wo 383   = wceq 1483   e. wcel 1990   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  elpr2OLD  4200  nelpri  4201  nelprd  4203  tppreqb  4336  elpreqpr  4396  elpr2elpr  4398  prproe  4434  3elpr2eq  4435  opth1  4944  0nelop  4960  funtpgOLD  5943  ftpg  6423  2oconcl  7583  cantnflem2  8587  m1expcl2  12882  hash2pwpr  13258  bitsinv1lem  15163  prm23lt5  15519  xpscfv  16222  xpsfeq  16224  pmtrprfval  17907  m1expaddsub  17918  psgnprfval  17941  frgpuptinv  18184  frgpup3lem  18190  cnmsgnsubg  19923  zrhpsgnelbas  19940  mdetralt  20414  m2detleiblem1  20430  indiscld  20895  cnindis  21096  connclo  21218  txindis  21437  xpsxmetlem  22184  xpsmet  22187  ishl2  23166  recnprss  23668  recnperf  23669  dvlip2  23758  coseq0negpitopi  24255  pythag  24547  reasinsin  24623  scvxcvx  24712  perfectlem2  24955  lgslem4  25025  lgseisenlem2  25101  2lgsoddprmlem3  25139  usgredg4  26109  konigsberg  27119  ex-pr  27287  elpreq  29360  1neg1t1neg1  29514  signswch  30638  kur14lem7  31194  poimirlem31  33440  ftc1anclem2  33486  wepwsolem  37612  relexp01min  38005  clsk1indlem1  38343  ssrecnpr  38507  seff  38508  sblpnf  38509  expgrowthi  38532  dvconstbi  38533  sumpair  39194  refsum2cnlem1  39196  iooinlbub  39723  elprn1  39865  elprn2  39866  cncfiooicclem1  40106  dvmptconst  40129  dvmptidg  40131  dvmulcncf  40140  dvdivcncf  40142  elprneb  41296  perfectALTVlem2  41631  0dig2pr01  42404