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

Theorem elpr 4047
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
Assertion
Ref Expression
elpr

Proof of Theorem elpr
StepHypRef Expression
1 elpr.1 . 2
2 elprg 4045 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  \/wo 368  =wceq 1395  e.wcel 1818   cvv 3109  {cpr 4031
This theorem is referenced by:  difprsnss  4165  preqr1  4204  preq12b  4206  prel12  4207  pwpr  4245  pwtp  4246  unipr  4262  intpr  4320  axpr  4690  zfpair2  4692  elop  4718  opthwiener  4754  xpsspw  5121  fnprb  6129  fnprOLD  6130  2oconcl  7172  pw2f1olem  7641  sdom2en01  8703  gruun  9205  fzpr  11764  isprm2  14225  drngnidl  17877  psgninv  18618  psgnodpm  18624  mdetunilem7  19120  indistopon  19502  dfcon2  19920  cnconn  19923  uncon  19930  txindis  20135  txcon  20190  filcon  20384  xpsdsval  20884  rolle  22391  dvivthlem1  22409  ang180lem3  23143  ang180lem4  23144  wilthlem2  23343  sqff1o  23456  ppiub  23479  lgslem1  23571  lgsdir2lem4  23601  lgsdir2lem5  23602  usgraexmpl  24401  3vfriswmgralem  25004  signslema  28519  subfacp1lem1  28623  subfacp1lem4  28627  m1expevenALT  28663  nosgnn0  29418  bpoly2  29819  bpoly3  29820  rankeq1o  29828  onsucconi  29902  divrngidl  30425  isfldidl  30465  wopprc  30972  pw2f1ocnv  30979  kelac2lem  31010  cncfiooicclem1  31696  tpres  32554  gsumpr  32950  dihmeetlem2N  37026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032
  Copyright terms: Public domain W3C validator