Theorem elpri 3583

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 3580	. 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 1335   e. wcel 2128   {cpr 3561

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567

This theorem is referenced by:  nelpri  3584  nelprd  3586  opth1  4196  0nelop  4208  ontr2exmid  4483  onintexmid  4531  reg3exmidlemwe  4537  funtpg  5220  ftpg  5650  acexmidlemcase  5816  2oconcl  6383  el2oss1o  6387  en2eqpr  6849  eldju1st  7009  nninfisol  7070  finomni  7077  exmidomniim  7078  ismkvnex  7092  exmidonfinlem  7122  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  exmidaclem  7137  sup3exmid  8822  m1expcl2  10434  maxleim  11098  maxleast  11106  zmaxcl  11117  minmax  11122  xrmaxleim  11134  xrmaxaddlem  11150  xrminmax  11155  unct  12154  qtopbas  12893  limcimolemlt  13004  recnprss  13027  coseq0negpitopi  13128  012of  13538  2o01f  13539  nninfalllem1  13551  nninfall  13552  nninfsellemqall  13558  nninfomnilem  13561  trilpolemclim  13578  trilpolemcl  13579  trilpolemisumle  13580  trilpolemeq1  13582  trilpolemlt1  13583  iswomni0  13593  nconstwlpolemgt0  13605  nconstwlpolem  13606