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

Theorem elpri 3660
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 3657 . 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 1623    e. wcel 1684   {cpr 3641
This theorem is referenced by:  nelpri  3661  opth1  4244  0nelop  4256  2oconcl  6502  cantnflem2  7392  m1expcl2  11125  bitsinv1lem  12632  xpscfv  13464  xpsfeq  13466  frgpuptinv  15080  frgpup3lem  15086  indiscld  16828  cnindis  17020  conclo  17141  txindis  17328  xpsxmetlem  17943  xpsmet  17946  ishl2  18787  recnprss  19254  recnperf  19255  dvlip2  19342  coseq0negpitopi  19871  pythag  20115  reasinsin  20192  scvxcvx  20280  perfectlem2  20469  lgslem4  20538  lgseisenlem2  20589  ex-pr  20817  kur14lem7  23154  vdgr1a  23308  konigsberg  23322  wepwsolem  26550  m1expaddsub  26833  cnmsgnsubg  26846  ssrecnpr  26949  seff  26950  sblpnf  26951  expgrowthi  26962  dvconstbi  26963  sumpair  27118  refsum2cnlem1  27120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator