Theorem elpri 3598

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

Syntax hints:   -> wi 4   \/ wo 698   = wceq 1343   e. wcel 2136   {cpr 3576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582

This theorem is referenced by:  nelpri  3599  nelprd  3601  opth1  4213  0nelop  4225  ontr2exmid  4501  onintexmid  4549  reg3exmidlemwe  4555  funtpg  5238  ftpg  5668  acexmidlemcase  5836  2oconcl  6403  el2oss1o  6407  en2eqpr  6869  eldju1st  7032  nninfisol  7093  finomni  7100  exmidomniim  7101  ismkvnex  7115  exmidonfinlem  7145  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  sup3exmid  8848  m1expcl2  10473  maxleim  11143  maxleast  11151  zmaxcl  11162  minmax  11167  xrmaxleim  11181  xrmaxaddlem  11197  xrminmax  11202  prm23lt5  12191  unct  12371  qtopbas  13122  limcimolemlt  13233  recnprss  13256  coseq0negpitopi  13357  lgslem4  13504  012of  13835  2o01f  13836  nninfalllem1  13848  nninfall  13849  nninfsellemqall  13855  nninfomnilem  13858  trilpolemclim  13875  trilpolemcl  13876  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  iswomni0  13890  nconstwlpolemgt0  13902  nconstwlpolem  13903