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  4378  0nelop  4390  ontr2exmid  4674  onintexmid  4722  reg3exmidlemwe  4728  funtpg  5435  ftpg  5902  acexmidlemcase  6083  2oconcl  6716  el2oss1o  6720  pw2f1odclem  7138  en2eqpr  7218  2omap  7324  eldju1st  7417  nninfisol  7479  finomni  7486  exmidomniim  7487  ismkvnex  7501  nninfwlpoimlemginf  7522  pr2cv1  7547  exmidonfinlem  7551  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  sup3exmid  9295  m1expcl2  11019  maxleim  11994  maxleast  12002  zmaxcl  12013  minmax  12020  zmincl  12029  xrmaxleim  12035  xrmaxaddlem  12051  xrminmax  12056  bitsinv1lem  12753  nninfctlemfo  12842  prm23lt5  13071  unct  13391  fnpr2ob  13720  fvprif  13723  xpsfeq  13725  qtopbas  15748  limcimolemlt  15890  recnprss  15913  dvmptid  15942  dvmptc  15943  coseq0negpitopi  16063  perfectlem2  16300  lgslem4  16327  lgseisenlem2  16395  2lgslem3  16425  2lgsoddprmlem3  16435  usgredg4  16661  vdegp1aid  16760  konigsberg  16939  012of  17228  2o01f  17229  idjudju  17252  nninfalllem1  17257  nninfall  17258  nninfsellemqall  17264  nninfomnilem  17267  nnnninfex  17271  nninfnfiinf  17272  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  iswomni0  17308  nconstwlpolemgt0  17321  nconstwlpolem  17322