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

Theorem elpr 3856
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 3855 . 2  |-  ( A  e.  _V  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
31, 2ax-mp 5 1  |-  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    \/ wo 359    = wceq 1653    e. wcel 1727   _Vcvv 2962   {cpr 3839
This theorem is referenced by:  difprsnss  3958  preqr1  3996  preq12b  3998  prel12  3999  pwpr  4035  pwtp  4036  unipr  4053  intpr  4107  axpr  4431  zfpair2  4433  elop  4458  opthwiener  4487  xpsspw  5015  fnpr  5979  fnprOLD  5980  2oconcl  6776  pw2f1olem  7241  sdom2en01  8213  gruun  8712  renfdisj  9169  fzpr  11132  isprm2  13118  drngnidl  16331  indistopon  17096  dfcon2  17513  cnconn  17516  uncon  17523  txindis  17697  txcon  17752  filcon  17946  xpsdsval  18442  rolle  19905  dvivthlem1  19923  ang180lem3  20684  ang180lem4  20685  wilthlem2  20883  sqff1o  20996  ppiub  21019  perfectlem2  21045  lgslem1  21111  lgsdir2lem4  21141  lgsdir2lem5  21142  usgraexmpl  21451  subfacp1lem1  24896  subfacp1lem4  24900  m1expevenALT  24936  nosgnn0  25644  bpoly2  26134  bpoly3  26135  rankeq1o  26143  onsucconi  26218  divrngidl  26676  isfldidl  26716  wopprc  27139  pw2f1ocnv  27146  kelac2lem  27177  3vfriswmgralem  28492  dihmeetlem2N  32195
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