Theorem elpri 3656

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 3653	. 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 710   = wceq 1373   e. wcel 2176   {cpr 3634

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640

This theorem is referenced by:  nelpri  3657  nelprd  3659  opth1  4281  0nelop  4293  ontr2exmid  4574  onintexmid  4622  reg3exmidlemwe  4628  funtpg  5326  ftpg  5770  acexmidlemcase  5941  2oconcl  6527  el2oss1o  6531  pw2f1odclem  6933  en2eqpr  7006  eldju1st  7175  nninfisol  7237  finomni  7244  exmidomniim  7245  ismkvnex  7259  nninfwlpoimlemginf  7280  exmidonfinlem  7303  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidaclem  7322  sup3exmid  9032  m1expcl2  10708  maxleim  11549  maxleast  11557  zmaxcl  11568  minmax  11574  xrmaxleim  11588  xrmaxaddlem  11604  xrminmax  11609  bitsinv1lem  12305  nninfctlemfo  12394  prm23lt5  12619  unct  12846  fnpr2ob  13205  fvprif  13208  xpsfeq  13210  qtopbas  15027  limcimolemlt  15169  recnprss  15192  dvmptid  15221  dvmptc  15222  coseq0negpitopi  15341  perfectlem2  15505  lgslem4  15513  lgseisenlem2  15581  2lgslem3  15611  2lgsoddprmlem3  15621  012of  15967  2o01f  15968  2omap  15969  nninfalllem1  15982  nninfall  15983  nninfsellemqall  15989  nninfomnilem  15992  nnnninfex  15996  nninfnfiinf  15997  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  iswomni0  16027  nconstwlpolemgt0  16040  nconstwlpolem  16041