Theorem elpri 3902

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 3898	. 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 1369   e. wcel 1756   {cpr 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-un 3338  df-sn 3883  df-pr 3885

This theorem is referenced by:  nelpri  3903  nelprd  3904  tppreqb  4019  opth1  4570  0nelop  4586  funtpg  5473  ftpg  5897  2oconcl  6948  cantnflem2  7903  m1expcl2  11892  hash2prd  12186  hash2pwpr  12187  bitsinv1lem  13642  xpscfv  14505  xpsfeq  14507  pmtrprfval  15998  m1expaddsub  16009  psgnprfval  16030  frgpuptinv  16273  frgpup3lem  16279  cnmsgnsubg  18012  zrhpsgnelbas  18029  mdetralt  18419  m2detleiblem1  18435  indiscld  18700  cnindis  18901  conclo  19024  txindis  19212  xpsxmetlem  19959  xpsmet  19962  ishl2  20887  recnprss  21384  recnperf  21385  dvlip2  21472  coseq0negpitopi  21970  pythag  22218  reasinsin  22296  scvxcvx  22384  perfectlem2  22574  lgslem4  22643  lgseisenlem2  22694  usgraedg4  23310  cusgrares  23385  2pthlem2  23500  vdgr1a  23581  konigsberg  23613  ex-pr  23642  elpreq  25905  signswch  26967  kur14lem7  27105  ftc1anclem2  28473  wepwsolem  29399  ssrecnpr  29599  seff  29600  sblpnf  29601  expgrowthi  29612  dvconstbi  29613  sumpair  29762  refsum2cnlem1  29764