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

Theorem elpri 3858
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 3855 . 2  |-  ( A  e.  { B ,  C }  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
21ibi 234 1  |-  ( A  e.  { B ,  C }  ->  ( A  =  B  \/  A  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359    = wceq 1653    e. wcel 1727   {cpr 3839
This theorem is referenced by:  nelpri  3859  tppreqb  3963  opth1  4463  0nelop  4475  funtpg  5530  ftpg  5945  2oconcl  6776  cantnflem2  7675  m1expcl2  11434  bitsinv1lem  12984  xpscfv  13818  xpsfeq  13820  frgpuptinv  15434  frgpup3lem  15440  indiscld  17186  cnindis  17387  conclo  17509  txindis  17697  xpsxmetlem  18440  xpsmet  18443  ishl2  19355  recnprss  19822  recnperf  19823  dvlip2  19910  coseq0negpitopi  20442  pythag  20690  reasinsin  20767  scvxcvx  20855  perfectlem2  21045  lgslem4  21114  lgseisenlem2  21165  usgraedg4  21437  cusgrares  21512  2pthlem2  21627  vdgr1a  21708  konigsberg  21740  ex-pr  21769  elpreq  24030  kur14lem7  24929  ftc1anclem2  26319  wepwsolem  27154  m1expaddsub  27436  cnmsgnsubg  27449  ssrecnpr  27552  seff  27553  sblpnf  27554  expgrowthi  27565  dvconstbi  27566  sumpair  27720  refsum2cnlem1  27722  nelprd  28093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311  df-sn 3844  df-pr 3845
  Copyright terms: Public domain W3C validator