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

Theorem elpr 3659
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 3658 . 2  |-  ( A  e.  _V  ->  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) ) )
31, 2ax-mp 10 1  |-  ( A  e.  { B ,  C }  <->  ( A  =  B  \/  A  =  C ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    \/ wo 359    = wceq 1624    e. wcel 1685   _Vcvv 2789   {cpr 3642
This theorem is referenced by:  difprsn  3757  preqr1  3787  preq12b  3789  prel12  3790  pwpr  3824  pwtp  3825  unipr  3842  intpr  3896  axpr  4212  zfpair2  4214  elop  4238  opthwiener  4267  xpsspw  4796  2oconcl  6497  pw2f1olem  6961  sdom2en01  7923  gruun  8423  renfdisj  8880  fzpr  10834  isprm2  12760  drngnidl  15975  indistopon  16732  dfcon2  17139  cnconn  17142  uncon  17149  txindis  17322  txcon  17377  filcon  17572  xpsdsval  17939  rolle  19331  dvivthlem1  19349  ang180lem3  20103  ang180lem4  20104  wilthlem2  20301  sqff1o  20414  ppiub  20437  perfectlem2  20463  lgslem1  20529  lgsdir2lem4  20559  lgsdir2lem5  20560  subfacp1lem1  23114  subfacp1lem4  23118  nosgnn0  23712  bpoly2  24199  bpoly3  24200  rankeq1o  24208  onsucconi  24283  cntrset  25001  fnckle  25444  pfsubkl  25446  abhp2  25574  divrngidl  26052  isfldidl  26092  wopprc  26522  pw2f1ocnv  26529  kelac2lem  26561  dihmeetlem2N  30756
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-sn 3647  df-pr 3648
  Copyright terms: Public domain W3C validator