Theorem elpri 3642

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 3639	. 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 2164   {cpr 3620

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626

This theorem is referenced by:  nelpri  3643  nelprd  3645  opth1  4266  0nelop  4278  ontr2exmid  4558  onintexmid  4606  reg3exmidlemwe  4612  funtpg  5306  ftpg  5743  acexmidlemcase  5914  2oconcl  6494  el2oss1o  6498  pw2f1odclem  6892  en2eqpr  6965  eldju1st  7132  nninfisol  7194  finomni  7201  exmidomniim  7202  ismkvnex  7216  nninfwlpoimlemginf  7237  exmidonfinlem  7255  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  sup3exmid  8978  m1expcl2  10635  maxleim  11352  maxleast  11360  zmaxcl  11371  minmax  11376  xrmaxleim  11390  xrmaxaddlem  11406  xrminmax  11411  nninfctlemfo  12180  prm23lt5  12404  unct  12602  fnpr2ob  12926  fvprif  12929  xpsfeq  12931  qtopbas  14701  limcimolemlt  14843  recnprss  14866  dvmptid  14895  dvmptc  14896  coseq0negpitopi  15012  lgslem4  15160  lgseisenlem2  15228  2lgslem3  15258  2lgsoddprmlem3  15268  012of  15556  2o01f  15557  nninfalllem1  15568  nninfall  15569  nninfsellemqall  15575  nninfomnilem  15578  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  iswomni0  15611  nconstwlpolemgt0  15624  nconstwlpolem  15625