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

Definition df-pr 3916
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, Ae.{1,-u1}->(A 2)=1 (ex-pr 22759). They are unordered, so as proven by prcom 3982. For a more traditional definition, but requiring a dummy variable, see dfpr2 3925. (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 3910 . 2
41csn 3909 . . 3
52csn 3909 . . 3
64, 5cun 3363 . 2
73, 6wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3923  dfpr2  3925  ralprg  3957  rexprg  3958  disjpr2  3970  prcom  3982  preq1  3983  qdass  4003  qdassr  4004  tpidm12  4005  prprc1  4014  difprsn1  4035  diftpsn3  4037  tpprceq3  4038  snsspr1  4047  snsspr2  4048  prss  4052  prssg  4053  ssunpr  4061  sstp  4063  pwssun  4648  xpsspw  4975  xpsspwOLD  4976  dmpropg  5332  rnpropg  5339  funprg  5485  funtp  5488  fntpg  5491  f1oprswap  5697  f1oprg  5698  fnimapr  5771  residpr  5901  fpr  5905  fmptpr  5918  fvpr1  5936  fvpr1g  5938  fvpr2g  5939  df2o3  6899  map2xp  7442  1sdom  7476  en2  7509  prfi  7547  prwf  7904  rankprb  7944  pr2nelem  8057  xp2cda  8231  ssxr  9323  prunioo  11275  hashprg  12004  hashprlei  12026  s2prop  12371  s4prop  12372  f1oun2prg  12374  isprm2lem  13617  strlemor2  14111  strle2  14115  phlstr  14162  xpscg  14337  symg2bas  15684  dmdprdpr  16222  dprdpr  16223  lsmpr  16784  lsppr  16788  lspsntri  16792  lsppratlem1  16842  lsppratlem3  16844  lsppratlem4  16845  m2detleib  17909  xpstopnlem1  18856  ovolioo  20477  uniiccdif  20485  i1f1  20595  wilthlem2  21873  perfectlem2  22035  constr2spthlem1  22615  constr3pthlem1  22663  constr3pthlem2  22664  ex-dif  22752  ex-un  22753  ex-in  22754  ex-xp  22765  ex-cnv  22766  ex-rn  22769  ex-res  22770  spanpr  24105  superpos  24880  prct  25142  sumpr  25399  esumpr  25696  eulerpartgbij  25929  signswch  26113  subfacp1lem1  26213  altopthsn  27145  axlowdimlem13  27232  onint1  27538  smprngopr  28034  sumpair  28932  csbprg  29296  difpr  29306  iunxprg  29315  rnfdmpr  29330  fzosplitpr  29404  fzosplitprm1  29405  gsumpr  29897  dihprrnlem1N  33772  dihprrnlem2  33773  djhlsmat  33775  lclkrlem2c  33857  lclkrlem2v  33876  lcfrlem18  33908
  Copyright terms: Public domain W3C validator