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

Theorem elpr 3824
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 3823 . 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 177    \/ wo 358    = wceq 1652    e. wcel 1725   _Vcvv 2948   {cpr 3807
This theorem is referenced by:  difprsnss  3926  preqr1  3964  preq12b  3966  prel12  3967  pwpr  4003  pwtp  4004  unipr  4021  intpr  4075  axpr  4394  zfpair2  4396  elop  4421  opthwiener  4450  xpsspw  4977  fnpr  5941  fnprOLD  5942  2oconcl  6738  pw2f1olem  7203  sdom2en01  8171  gruun  8670  renfdisj  9127  fzpr  11090  isprm2  13075  drngnidl  16288  indistopon  17053  dfcon2  17470  cnconn  17473  uncon  17480  txindis  17654  txcon  17709  filcon  17903  xpsdsval  18399  rolle  19862  dvivthlem1  19880  ang180lem3  20641  ang180lem4  20642  wilthlem2  20840  sqff1o  20953  ppiub  20976  perfectlem2  21002  lgslem1  21068  lgsdir2lem4  21098  lgsdir2lem5  21099  usgraexmpl  21408  subfacp1lem1  24853  subfacp1lem4  24857  m1expevenALT  24893  nosgnn0  25567  bpoly2  26051  bpoly3  26052  rankeq1o  26060  onsucconi  26135  divrngidl  26575  isfldidl  26615  wopprc  27038  pw2f1ocnv  27045  kelac2lem  27077  3vfriswmgralem  28252  dihmeetlem2N  31936
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-sn 3812  df-pr 3813
  Copyright terms: Public domain W3C validator