Theorem elpri 3997

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

Syntax hints:   -> wi 4   \/ wo 374   = wceq 1455   e. wcel 1898   {cpr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-sn 3981  df-pr 3983

This theorem is referenced by:  elpr2  3999  nelpri  4000  nelprd  4001  tppreqb  4126  elpreqpr  4175  opth1  4692  0nelop  4708  funtpg  5655  ftpg  6103  2oconcl  7236  cantnflem2  8226  m1expcl2  12332  hash2pwpr  12674  bitsinv1lem  14470  xpscfv  15523  xpsfeq  15525  pmtrprfval  17183  m1expaddsub  17194  psgnprfval  17217  frgpuptinv  17476  frgpup3lem  17482  cnmsgnsubg  19200  zrhpsgnelbas  19217  mdetralt  19688  m2detleiblem1  19704  indiscld  20162  cnindis  20363  conclo  20485  txindis  20704  xpsxmetlem  21449  xpsmet  21452  ishl2  22392  recnprss  22915  recnperf  22916  dvlip2  23003  coseq0negpitopi  23514  pythag  23802  reasinsin  23878  scvxcvx  23967  perfectlem2  24214  lgslem4  24283  lgseisenlem2  24334  usgraedg4  25170  cusgrares  25256  2pthlem2  25382  vdgr1a  25690  konigsberg  25771  ex-pr  25936  elpreq  28212  1neg1t1neg1  28377  signswch  29500  kur14lem7  29985  poimirlem31  32017  ftc1anclem2  32064  wepwsolem  35946  relexp01min  36351  ssrecnpr  36701  seff  36702  sblpnf  36703  expgrowthi  36727  dvconstbi  36728  sumpair  37397  refsum2cnlem1  37399  iooinlbub  37683  elprn1  37799  elprn2  37800  cncfiooicclem1  37857  dvmptconst  37871  dvmptidg  37873  dvmulcncf  37883  dvdivcncf  37885  elprneb  38847  perfectALTVlem2  38979  elpr2elpr  39140  usgredg4  39440  usgvincvad  40085  usgvincvadALT  40088  0dig2pr01  40790