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

Definition df-pr 3607
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 20746). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3665. For a more traditional definition, but requiring a dummy variable, see dfpr2 3616. (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 3601 . 2  class  { A ,  B }
41csn 3600 . . 3  class  { A }
52csn 3600 . . 3  class  { B }
64, 5cun 3111 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1619 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3614  dfpr2  3616  ralprg  3642  rexprg  3643  prcom  3665  preq1  3666  qdass  3686  qdassr  3687  tpidm12  3688  prprc1  3696  snsspr1  3724  snsspr2  3725  prss  3729  prssg  3730  ssunpr  3736  sstp  3738  pwssun  4257  xpsspw  4771  xpsspwOLD  4772  dmpropg  5119  funprg  5225  funtp  5227  f1oprswap  5439  fnimapr  5503  fpr  5624  fvpr1  5642  df2o3  6446  map2xp  6985  1sdom  7019  en2  7048  prfi  7085  prwf  7437  rankprb  7477  pr2nelem  7588  xp2cda  7760  ssxr  8846  prunioo  10716  hashprg  11319  hashprlei  11330  isprm2lem  12713  strlemor2  13184  strle2  13188  phlstr  13235  xpscg  13408  dmdprdpr  15232  dprdpr  15233  lsmpr  15790  lsppr  15794  lspsntri  15798  lsppratlem1  15848  lsppratlem3  15850  lsppratlem4  15851  xpstopnlem1  17448  ovolioo  18873  uniiccdif  18881  i1f1  18993  wilthlem2  20255  perfectlem2  20417  ex-dif  20739  ex-un  20740  ex-in  20741  ex-xp  20752  ex-cnv  20753  ex-rn  20756  ex-res  20757  spanpr  22105  superpos  22880  subfacp1lem1  23068  altopthsn  23856  axlowdimlem13  23943  onint1  24249  repfuntw  24513  pgapspf  25405  smprngopr  26030  sumpair  27060  dihprrnlem1N  30765  dihprrnlem2  30766  djhlsmat  30768  lclkrlem2c  30850  lclkrlem2v  30869  lcfrlem18  30901
  Copyright terms: Public domain W3C validator