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

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

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cpr 3854 . 2
41csn 3853 . . 3
52csn 3853 . . 3
64, 5cun 3303 . 2
73, 6wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  3867  dfpr2  3869  ralprg  3902  rexprg  3903  disjpr2  3915  prcom  3928  preq1  3929  qdass  3949  qdassr  3950  tpidm12  3951  prprc1  3960  difprsn1  3985  diftpsn3  3987  tpprceq3  3988  snsspr1  3997  snsspr2  3998  prss  4002  prssg  4003  ssunpr  4010  sstp  4012  pwssun  4598  xpsspw  4924  xpsspwOLD  4925  dmpropg  5284  rnpropg  5291  funprg  5437  funtp  5440  fntpg  5443  f1oprswap  5650  f1oprg  5651  fnimapr  5725  residpr  5855  fpr  5859  fmptpr  5872  fvpr1  5890  fvpr1g  5892  fvpr2g  5893  df2o3  6894  map2xp  7440  1sdom  7474  en2  7507  prfi  7545  prwf  7965  rankprb  8005  pr2nelem  8118  xp2cda  8296  ssxr  9390  prunioo  11358  hashprg  12096  hashprlei  12118  s2prop  12465  s4prop  12466  f1oun2prg  12468  isprm2lem  13710  strlemor2  14206  strle2  14210  phlstr  14259  xpscg  14436  symg2bas  15840  dmdprdpr  16416  dprdpr  16417  lsmpr  16979  lsppr  16983  lspsntri  16987  lsppratlem1  17037  lsppratlem3  17039  lsppratlem4  17040  m2detleib  18139  xpstopnlem1  19086  ovolioo  20749  uniiccdif  20758  i1f1  20868  wilthlem2  22148  perfectlem2  22310  axlowdimlem13  22879  constr2spthlem1  23172  constr3pthlem1  23220  constr3pthlem2  23221  ex-dif  23309  ex-un  23310  ex-in  23311  ex-xp  23322  ex-cnv  23323  ex-rn  23326  ex-res  23327  spanpr  24662  superpos  25437  prct  25692  sumpr  25946  esumpr  26225  eulerpartgbij  26458  signswch  26665  subfacp1lem1  26770  altopthsn  27694  onint1  27998  smprngopr  28523  sumpair  29430  csbprg  29791  difpr  29799  iunxprg  29808  rnfdmpr  29823  fzosplitpr  29897  fzosplitprm1  29898  xpprsng  30393  gsumpr  30423  dihprrnlem1N  34506  dihprrnlem2  34507  djhlsmat  34509  lclkrlem2c  34591  lclkrlem2v  34610  lcfrlem18  34642
  Copyright terms: Public domain W3C validator