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

Theorem elpr 3671
Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)
Hypothesis
Ref Expression
elpr.1  |-  A  e. 
_V
Assertion
Ref Expression
elpr  |-  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) )

Proof of Theorem elpr
StepHypRef Expression
1 elpr.1 . 2  |-  A  e. 
_V
2 elprg 3670 . 2  |-  ( A  e.  _V  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
31, 2ax-mp 8 1  |-  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    = wceq 1632    e. wcel 1696   _Vcvv 2801   {cpr 3654
This theorem is referenced by:  difprsnss  3769  preqr1  3802  preq12b  3804  prel12  3805  pwpr  3839  pwtp  3840  unipr  3857  intpr  3911  axpr  4229  zfpair2  4231  elop  4255  opthwiener  4284  xpsspw  4813  2oconcl  6518  pw2f1olem  6982  sdom2en01  7944  gruun  8444  renfdisj  8901  fzpr  10856  isprm2  12782  drngnidl  15997  indistopon  16754  dfcon2  17161  cnconn  17164  uncon  17171  txindis  17344  txcon  17399  filcon  17594  xpsdsval  17961  rolle  19353  dvivthlem1  19371  ang180lem3  20125  ang180lem4  20126  wilthlem2  20323  sqff1o  20436  ppiub  20459  perfectlem2  20485  lgslem1  20551  lgsdir2lem4  20581  lgsdir2lem5  20582  subfacp1lem1  23725  subfacp1lem4  23729  nosgnn0  24383  bpoly2  24864  bpoly3  24865  rankeq1o  24873  onsucconi  24948  repfuntw  25263  cntrset  25705  fnckle  26148  pfsubkl  26150  abhp2  26278  divrngidl  26756  isfldidl  26796  wopprc  27226  pw2f1ocnv  27233  kelac2lem  27265  usgraexmpl  28267  3vfriswmgralem  28428  dihmeetlem2N  32111
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