Theorem elpri 3732

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 3729	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   \/ wo 720   = wceq 1402   e. wcel 2209   {cpr 3710

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716

This theorem is used by:  nelpri  3733  nelprd  3735  elpr2elpr  3901  opth1  4376  0nelop  4388  ontr2exmid  4672  onintexmid  4720  reg3exmidlemwe  4726  funtpg  5432  ftpg  5899  acexmidlemcase  6080  2oconcl  6712  el2oss1o  6716  pw2f1odclem  7134  en2eqpr  7214  2omap  7318  eldju1st  7411  nninfisol  7473  finomni  7480  exmidomniim  7481  ismkvnex  7495  nninfwlpoimlemginf  7516  pr2cv1  7541  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  sup3exmid  9287  m1expcl2  10998  maxleim  11971  maxleast  11979  zmaxcl  11990  minmax  11996  xrmaxleim  12010  xrmaxaddlem  12026  xrminmax  12031  bitsinv1lem  12728  nninfctlemfo  12817  prm23lt5  13042  unct  13333  fnpr2ob  13661  fvprif  13664  xpsfeq  13666  qtopbas  15623  limcimolemlt  15765  recnprss  15788  dvmptid  15817  dvmptc  15818  coseq0negpitopi  15937  perfectlem2  16114  lgslem4  16122  lgseisenlem2  16190  2lgslem3  16220  2lgsoddprmlem3  16230  usgredg4  16456  vdegp1aid  16555  konigsberg  16734  012of  17023  2o01f  17024  nninfalllem1  17051  nninfall  17052  nninfsellemqall  17058  nninfomnilem  17061  nnnninfex  17065  nninfnfiinf  17066  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  iswomni0  17101  nconstwlpolemgt0  17114  nconstwlpolem  17115