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

Definition df-pr 3650
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example,  A  e.  {
1 ,  -u 1 }  ->  ( A ^
2 )  =  1 (ex-pr 20794). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3708. For a more traditional definition, but requiring a dummy variable, see dfpr2 3659. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-pr  |-  { A ,  B }  =  ( { A }  u.  { B } )

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cpr 3644 . 2  class  { A ,  B }
41csn 3643 . . 3  class  { A }
52csn 3643 . . 3  class  { B }
64, 5cun 3153 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1625 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3657  dfpr2  3659  ralprg  3685  rexprg  3686  prcom  3708  preq1  3709  qdass  3729  qdassr  3730  tpidm12  3731  prprc1  3739  snsspr1  3767  snsspr2  3768  prss  3772  prssg  3773  ssunpr  3779  sstp  3781  pwssun  4300  xpsspw  4798  xpsspwOLD  4799  dmpropg  5146  funprg  5268  funtp  5270  f1oprswap  5482  fnimapr  5546  fpr  5667  fvpr1  5685  df2o3  6489  map2xp  7028  1sdom  7062  en2  7091  prfi  7128  prwf  7480  rankprb  7520  pr2nelem  7631  xp2cda  7803  ssxr  8889  prunioo  10760  hashprg  11364  hashprlei  11375  isprm2lem  12761  strlemor2  13232  strle2  13236  phlstr  13283  xpscg  13456  dmdprdpr  15280  dprdpr  15281  lsmpr  15838  lsppr  15842  lspsntri  15846  lsppratlem1  15896  lsppratlem3  15898  lsppratlem4  15899  xpstopnlem1  17496  ovolioo  18921  uniiccdif  18929  i1f1  19041  wilthlem2  20303  perfectlem2  20465  ex-dif  20787  ex-un  20788  ex-in  20789  ex-xp  20800  ex-cnv  20801  ex-rn  20804  ex-res  20805  spanpr  22153  superpos  22928  subfacp1lem1  23116  altopthsn  23904  axlowdimlem13  23991  onint1  24297  repfuntw  24561  pgapspf  25453  smprngopr  26078  sumpair  27107  dihprrnlem1N  30883  dihprrnlem2  30884  djhlsmat  30886  lclkrlem2c  30968  lclkrlem2v  30987  lcfrlem18  31019
  Copyright terms: Public domain W3C validator