Theorem elpri 3666

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 3663	. 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 710   = wceq 1373   e. wcel 2178   {cpr 3644

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650

This theorem is referenced by:  nelpri  3667  nelprd  3669  elpr2elpr  3830  opth1  4298  0nelop  4310  ontr2exmid  4591  onintexmid  4639  reg3exmidlemwe  4645  funtpg  5344  ftpg  5791  acexmidlemcase  5962  2oconcl  6548  el2oss1o  6552  pw2f1odclem  6956  en2eqpr  7030  eldju1st  7199  nninfisol  7261  finomni  7268  exmidomniim  7269  ismkvnex  7283  nninfwlpoimlemginf  7304  pr2cv1  7329  exmidonfinlem  7332  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidaclem  7351  sup3exmid  9065  m1expcl2  10743  maxleim  11631  maxleast  11639  zmaxcl  11650  minmax  11656  xrmaxleim  11670  xrmaxaddlem  11686  xrminmax  11691  bitsinv1lem  12387  nninfctlemfo  12476  prm23lt5  12701  unct  12928  fnpr2ob  13287  fvprif  13290  xpsfeq  13292  qtopbas  15109  limcimolemlt  15251  recnprss  15274  dvmptid  15303  dvmptc  15304  coseq0negpitopi  15423  perfectlem2  15587  lgslem4  15595  lgseisenlem2  15663  2lgslem3  15693  2lgsoddprmlem3  15703  012of  16130  2o01f  16131  2omap  16132  nninfalllem1  16147  nninfall  16148  nninfsellemqall  16154  nninfomnilem  16157  nnnninfex  16161  nninfnfiinf  16162  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  iswomni0  16192  nconstwlpolemgt0  16205  nconstwlpolem  16206