Theorem elpri 3555

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 3552	. 2 |- ( A e. { B , C } -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
2	1	ibi 175	1 |- ( A e. { B , C } -> ( A = B \/ A = C ) )

Syntax hints:   -> wi 4   \/ wo 698   = wceq 1332   e. wcel 1481   {cpr 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539

This theorem is referenced by:  nelpri  3556  nelprd  3558  opth1  4166  0nelop  4178  ontr2exmid  4448  onintexmid  4495  reg3exmidlemwe  4501  funtpg  5182  ftpg  5612  acexmidlemcase  5777  2oconcl  6344  en2eqpr  6809  eldju1st  6964  finomni  7020  exmidomniim  7021  ismkvnex  7037  exmidonfinlem  7066  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  sup3exmid  8739  m1expcl2  10346  maxleim  11009  maxleast  11017  zmaxcl  11028  minmax  11033  xrmaxleim  11045  xrmaxaddlem  11061  xrminmax  11066  unct  11991  qtopbas  12730  limcimolemlt  12841  recnprss  12864  coseq0negpitopi  12965  el2oss1o  13359  012of  13363  2o01f  13364  nninfalllem1  13378  nninfall  13379  nninfsellemqall  13386  nninfomnilem  13389  trilpolemclim  13404  trilpolemcl  13405  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409