Theorem elpri 3645

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

Syntax hints:   -> wi 4   \/ wo 709   = wceq 1364   e. wcel 2167   {cpr 3623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629

This theorem is referenced by:  nelpri  3646  nelprd  3648  opth1  4269  0nelop  4281  ontr2exmid  4561  onintexmid  4609  reg3exmidlemwe  4615  funtpg  5309  ftpg  5746  acexmidlemcase  5917  2oconcl  6497  el2oss1o  6501  pw2f1odclem  6895  en2eqpr  6968  eldju1st  7137  nninfisol  7199  finomni  7206  exmidomniim  7207  ismkvnex  7221  nninfwlpoimlemginf  7242  exmidonfinlem  7260  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  sup3exmid  8984  m1expcl2  10653  maxleim  11370  maxleast  11378  zmaxcl  11389  minmax  11395  xrmaxleim  11409  xrmaxaddlem  11425  xrminmax  11430  nninfctlemfo  12207  prm23lt5  12432  unct  12659  fnpr2ob  12983  fvprif  12986  xpsfeq  12988  qtopbas  14758  limcimolemlt  14900  recnprss  14923  dvmptid  14952  dvmptc  14953  coseq0negpitopi  15072  perfectlem2  15236  lgslem4  15244  lgseisenlem2  15312  2lgslem3  15342  2lgsoddprmlem3  15352  012of  15640  2o01f  15641  nninfalllem1  15652  nninfall  15653  nninfsellemqall  15659  nninfomnilem  15662  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  iswomni0  15695  nconstwlpolemgt0  15708  nconstwlpolem  15709