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

Definition df-pr 3850
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 21776). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3911. For a more traditional definition, but requiring a dummy variable, see dfpr2 3859. (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 3844 . 2  class  { A ,  B }
41csn 3843 . . 3  class  { A }
52csn 3843 . . 3  class  { B }
64, 5cun 3307 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1654 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3857  dfpr2  3859  ralprg  3886  rexprg  3887  disjpr2  3899  prcom  3911  preq1  3912  qdass  3932  qdassr  3933  tpidm12  3934  prprc1  3943  difprsn1  3964  diftpsn3  3966  tpprceq3  3967  snsspr1  3976  snsspr2  3977  prss  3981  prssg  3982  ssunpr  3990  sstp  3992  pwssun  4524  xpsspw  5021  xpsspwOLD  5022  dmpropg  5378  funprg  5535  funtp  5538  fntpg  5541  f1oprswap  5752  f1oprg  5753  fnimapr  5823  fpr  5950  fvpr1  5971  fvpr1g  5973  fvpr2g  5974  df2o3  6773  map2xp  7313  1sdom  7347  en2  7380  prfi  7417  prwf  7773  rankprb  7813  pr2nelem  7926  xp2cda  8098  ssxr  9183  prunioo  11063  hashprg  11704  hashprlei  11724  s2prop  11899  s4prop  11900  f1oun2prg  11902  isprm2lem  13124  strlemor2  13595  strle2  13599  phlstr  13646  xpscg  13821  dmdprdpr  15645  dprdpr  15646  lsmpr  16199  lsppr  16203  lspsntri  16207  lsppratlem1  16257  lsppratlem3  16259  lsppratlem4  16260  xpstopnlem1  17879  ovolioo  19500  uniiccdif  19508  i1f1  19618  wilthlem2  20890  perfectlem2  21052  constr2spthlem1  21632  constr3pthlem1  21680  constr3pthlem2  21681  ex-dif  21769  ex-un  21770  ex-in  21771  ex-xp  21782  ex-cnv  21783  ex-rn  21786  ex-res  21787  spanpr  23120  superpos  23895  rnpropg  24070  fmptpr  24097  prct  24139  sumpr  24253  esumpr  24492  subfacp1lem1  24900  altopthsn  25841  axlowdimlem13  25928  onint1  26234  smprngopr  26704  sumpair  27794  difpr  28172  iunxprg  28181  rnfdmpr  28199  dihprrnlem1N  32396  dihprrnlem2  32397  djhlsmat  32399  lclkrlem2c  32481  lclkrlem2v  32500  lcfrlem18  32532
  Copyright terms: Public domain W3C validator