Theorem elpri 3617

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 3614	. 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 708   = wceq 1353   e. wcel 2148   {cpr 3595

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601

This theorem is referenced by:  nelpri  3618  nelprd  3620  opth1  4238  0nelop  4250  ontr2exmid  4526  onintexmid  4574  reg3exmidlemwe  4580  funtpg  5269  ftpg  5703  acexmidlemcase  5873  2oconcl  6443  el2oss1o  6447  en2eqpr  6910  eldju1st  7073  nninfisol  7134  finomni  7141  exmidomniim  7142  ismkvnex  7156  nninfwlpoimlemginf  7177  exmidonfinlem  7195  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  exmidaclem  7210  sup3exmid  8917  m1expcl2  10545  maxleim  11217  maxleast  11225  zmaxcl  11236  minmax  11241  xrmaxleim  11255  xrmaxaddlem  11271  xrminmax  11276  prm23lt5  12266  unct  12446  fnpr2ob  12766  fvprif  12769  xpsfeq  12771  qtopbas  14210  limcimolemlt  14321  recnprss  14344  coseq0negpitopi  14445  lgslem4  14592  lgseisenlem2  14639  2lgsoddprmlem3  14647  012of  14934  2o01f  14935  nninfalllem1  14946  nninfall  14947  nninfsellemqall  14953  nninfomnilem  14956  trilpolemclim  14973  trilpolemcl  14974  trilpolemisumle  14975  trilpolemeq1  14977  trilpolemlt1  14978  iswomni0  14988  nconstwlpolemgt0  15001  nconstwlpolem  15002