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

Definition df-pr 4032
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, Ae.{1,-u1}->(A 2)=1 (ex-pr 25151). They are unordered, so as proven by prcom 4108. For a more traditional definition, but requiring a dummy variable, see dfpr2 4044. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
df-pr

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cpr 4031 . 2
41csn 4029 . . 3
52csn 4029 . . 3
64, 5cun 3473 . 2
73, 6wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  4042  dfpr2  4044  ralprg  4078  rexprg  4079  csbprg  4089  disjpr2  4092  prcom  4108  preq1  4109  qdass  4129  qdassr  4130  tpidm12  4131  prprc1  4140  difprsn1  4166  diftpsn3  4168  difpr  4169  tpprceq3  4170  snsspr1  4179  snsspr2  4180  prss  4184  prssg  4185  ssunpr  4192  sstp  4194  pwssun  4791  xpsspw  5121  xpsspwOLD  5122  dmpropg  5486  rnpropg  5493  funprg  5642  funtp  5645  fntpg  5648  f1oprswap  5860  f1oprg  5861  fnimapr  5937  residpr  6075  fpr  6079  fmptpr  6096  fvpr1  6114  fvpr1g  6116  fvpr2g  6117  df2o3  7162  map2xp  7707  1sdom  7742  en2  7776  prfi  7815  prwf  8250  rankprb  8290  pr2nelem  8403  xp2cda  8581  ssxr  9675  prunioo  11678  fzosplitprm1  11919  hashprg  12460  hashprlei  12514  s2prop  12862  s4prop  12863  f1oun2prg  12865  isprm2lem  14224  strlemor2  14725  strle2  14729  phlstr  14778  xpscg  14955  symg2bas  16423  dmdprdpr  17098  dprdpr  17099  lsmpr  17735  lsppr  17739  lspsntri  17743  lsppratlem1  17793  lsppratlem3  17795  lsppratlem4  17796  m2detleib  19133  xpstopnlem1  20310  ovolioo  21978  uniiccdif  21987  i1f1  22097  wilthlem2  23343  perfectlem2  23505  axlowdimlem13  24257  nbgraopALT  24424  constr2spthlem1  24596  constr3pthlem1  24655  constr3pthlem2  24656  ex-dif  25144  ex-un  25145  ex-in  25146  ex-xp  25157  ex-cnv  25158  ex-rn  25161  ex-res  25162  spanpr  26498  superpos  27273  prct  27535  sumpr  27769  esumpr  28073  eulerpartgbij  28311  signswch  28518  subfacp1lem1  28623  altopthsn  29611  onint1  29914  smprngopr  30449  sumpair  31410  iunxprg  32302  rnfdmpr  32308  fzosplitpr  32342  xpprsng  32921  gsumpr  32950  dihprrnlem1N  37151  dihprrnlem2  37152  djhlsmat  37154  lclkrlem2c  37236  lclkrlem2v  37255  lcfrlem18  37287
  Copyright terms: Public domain W3C validator