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

Definition df-pr 3647
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 20817). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3705. For a more traditional definition, but requiring a dummy variable, see dfpr2 3656. (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 3641 . 2  class  { A ,  B }
41csn 3640 . . 3  class  { A }
52csn 3640 . . 3  class  { B }
64, 5cun 3150 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1623 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3654  dfpr2  3656  ralprg  3682  rexprg  3683  prcom  3705  preq1  3706  qdass  3726  qdassr  3727  tpidm12  3728  prprc1  3736  snsspr1  3764  snsspr2  3765  prss  3769  prssg  3770  ssunpr  3776  sstp  3778  pwssun  4299  xpsspw  4797  xpsspwOLD  4798  dmpropg  5146  funprg  5301  funtp  5303  f1oprswap  5515  fnimapr  5583  fpr  5704  fvpr1  5722  df2o3  6492  map2xp  7031  1sdom  7065  en2  7094  prfi  7131  prwf  7483  rankprb  7523  pr2nelem  7634  xp2cda  7806  ssxr  8892  prunioo  10764  hashprg  11368  hashprlei  11379  isprm2lem  12765  strlemor2  13236  strle2  13240  phlstr  13287  xpscg  13460  dmdprdpr  15284  dprdpr  15285  lsmpr  15842  lsppr  15846  lspsntri  15850  lsppratlem1  15900  lsppratlem3  15902  lsppratlem4  15903  xpstopnlem1  17500  ovolioo  18925  uniiccdif  18933  i1f1  19045  wilthlem2  20307  perfectlem2  20469  ex-dif  20810  ex-un  20811  ex-in  20812  ex-xp  20823  ex-cnv  20824  ex-rn  20827  ex-res  20828  spanpr  22159  superpos  22934  sumpr  23168  rnpropg  23189  difprsn2  23191  fmptpr  23214  prct  23340  esumpr  23438  subfacp1lem1  23710  altopthsn  24495  axlowdimlem13  24582  onint1  24888  pgapspf  26052  smprngopr  26677  sumpair  27706  difprsneq  28068  difprsng  28069  diftpsneq  28070  tpprceq3  28072  f1oprg  28075  f1oun2prg  28076  s2prop  28089  s4prop  28090  dihprrnlem1N  31614  dihprrnlem2  31615  djhlsmat  31617  lclkrlem2c  31699  lclkrlem2v  31718  lcfrlem18  31750
  Copyright terms: Public domain W3C validator