MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpri Unicode version

Theorem elpri 3779
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
StepHypRef Expression
1 elprg 3776 . 2  |-  ( A  e.  { B ,  C }  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
21ibi 233 1  |-  ( A  e.  { B ,  C }  ->  ( A  =  B  \/  A  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    = wceq 1649    e. wcel 1717   {cpr 3760
This theorem is referenced by:  nelpri  3780  tppreqb  3884  opth1  4377  0nelop  4389  funtpg  5443  ftpg  5857  2oconcl  6685  cantnflem2  7581  m1expcl2  11332  bitsinv1lem  12882  xpscfv  13716  xpsfeq  13718  frgpuptinv  15332  frgpup3lem  15338  indiscld  17080  cnindis  17280  conclo  17401  txindis  17589  xpsxmetlem  18319  xpsmet  18322  ishl2  19193  recnprss  19660  recnperf  19661  dvlip2  19748  coseq0negpitopi  20280  pythag  20528  reasinsin  20605  scvxcvx  20693  perfectlem2  20883  lgslem4  20952  lgseisenlem2  21003  usgraedg4  21274  cusgrares  21349  2pthonlem2  21450  vdgr1a  21527  konigsberg  21559  ex-pr  21588  elpreq  23845  kur14lem7  24679  wepwsolem  26809  m1expaddsub  27092  cnmsgnsubg  27105  ssrecnpr  27208  seff  27209  sblpnf  27210  expgrowthi  27221  dvconstbi  27222  sumpair  27376  refsum2cnlem1  27378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-un 3270  df-sn 3765  df-pr 3766
  Copyright terms: Public domain W3C validator