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

Theorem elpr 3658
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 3657 . 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 1623    e. wcel 1684   _Vcvv 2788   {cpr 3641
This theorem is referenced by:  difprsn  3756  preqr1  3786  preq12b  3788  prel12  3789  pwpr  3823  pwtp  3824  unipr  3841  intpr  3895  axpr  4213  zfpair2  4215  elop  4239  opthwiener  4268  xpsspw  4797  2oconcl  6502  pw2f1olem  6966  sdom2en01  7928  gruun  8428  renfdisj  8885  fzpr  10840  isprm2  12766  drngnidl  15981  indistopon  16738  dfcon2  17145  cnconn  17148  uncon  17155  txindis  17328  txcon  17383  filcon  17578  xpsdsval  17945  rolle  19337  dvivthlem1  19355  ang180lem3  20109  ang180lem4  20110  wilthlem2  20307  sqff1o  20420  ppiub  20443  perfectlem2  20469  lgslem1  20535  lgsdir2lem4  20565  lgsdir2lem5  20566  subfacp1lem1  23710  subfacp1lem4  23714  nosgnn0  24312  bpoly2  24792  bpoly3  24793  rankeq1o  24801  onsucconi  24876  repfuntw  25160  cntrset  25602  fnckle  26045  pfsubkl  26047  abhp2  26175  divrngidl  26653  isfldidl  26693  wopprc  27123  pw2f1ocnv  27130  kelac2lem  27162  usgraexmpl  28133  3vfriswmgralem  28182  dihmeetlem2N  31489
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