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

Theorem elpri 3673
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 3670 . 2  |-  ( A  e.  { B ,  C }  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
21ibi 232 1  |-  ( A  e.  { B ,  C }  ->  ( A  =  B  \/  A  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    = wceq 1632    e. wcel 1696   {cpr 3654
This theorem is referenced by:  nelpri  3674  opth1  4260  0nelop  4272  2oconcl  6518  cantnflem2  7408  m1expcl2  11141  bitsinv1lem  12648  xpscfv  13480  xpsfeq  13482  frgpuptinv  15096  frgpup3lem  15102  indiscld  16844  cnindis  17036  conclo  17157  txindis  17344  xpsxmetlem  17959  xpsmet  17962  ishl2  18803  recnprss  19270  recnperf  19271  dvlip2  19358  coseq0negpitopi  19887  pythag  20131  reasinsin  20208  scvxcvx  20296  perfectlem2  20485  lgslem4  20554  lgseisenlem2  20605  ex-pr  20833  elpreq  23204  kur14lem7  23758  vdgr1a  23912  konigsberg  23926  wepwsolem  27241  m1expaddsub  27524  cnmsgnsubg  27537  ssrecnpr  27640  seff  27641  sblpnf  27642  expgrowthi  27653  dvconstbi  27654  sumpair  27809  refsum2cnlem1  27811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator