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

Theorem elpr 3562
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 3561 . 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 1619    e. wcel 1621   _Vcvv 2727   {cpr 3545
This theorem is referenced by:  difprsn  3658  preqr1  3686  preq12b  3688  prel12  3689  pwpr  3723  pwtp  3724  unipr  3741  intpr  3793  axpr  4107  zfpair2  4109  elop  4132  opthwiener  4161  xpsspw  4704  2oconcl  6388  pw2f1olem  6851  sdom2en01  7812  gruun  8308  renfdisj  8765  fzpr  10718  isprm2  12640  drngnidl  15813  indistopon  16570  dfcon2  16977  cnconn  16980  uncon  16987  txindis  17160  txcon  17215  filcon  17410  xpsdsval  17777  rolle  19169  dvivthlem1  19187  ang180lem3  19853  ang180lem4  19854  wilthlem2  20139  sqff1o  20252  ppiub  20275  perfectlem2  20301  lgslem1  20367  lgsdir2lem4  20397  lgsdir2lem5  20398  subfacp1lem1  22881  subfacp1lem4  22885  nosgnn0  23479  bpoly2  23966  bpoly3  23967  rankeq1o  23975  onsucconi  24050  cntrset  24768  fnckle  25211  pfsubkl  25213  abhp2  25341  divrngidl  25819  isfldidl  25859  wopprc  26289  pw2f1ocnv  26296  kelac2lem  26328  dihmeetlem2N  30178
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-sn 3550  df-pr 3551
  Copyright terms: Public domain W3C validator