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  9289  m1expcl2  11011  maxleim  11986  maxleast  11994  zmaxcl  12005  minmax  12011  zmincl  12020  xrmaxleim  12026  xrmaxaddlem  12042  xrminmax  12047  bitsinv1lem  12744  nninfctlemfo  12833  prm23lt5  13062  unct  13382  fnpr2ob  13710  fvprif  13713  xpsfeq  13715  qtopbas  15672  limcimolemlt  15814  recnprss  15837  dvmptid  15866  dvmptc  15867  coseq0negpitopi  15987  perfectlem2  16198  lgslem4  16220  lgseisenlem2  16288  2lgslem3  16318  2lgsoddprmlem3  16328  usgredg4  16554  vdegp1aid  16653  konigsberg  16832  012of  17121  2o01f  17122  nninfalllem1  17149  nninfall  17150  nninfsellemqall  17156  nninfomnilem  17159  nnnninfex  17163  nninfnfiinf  17164  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  iswomni0  17199  nconstwlpolemgt0  17212  nconstwlpolem  17213