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

Definition df-pr 3660
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 20833). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3718. For a more traditional definition, but requiring a dummy variable, see dfpr2 3669. (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 3654 . 2  class  { A ,  B }
41csn 3653 . . 3  class  { A }
52csn 3653 . . 3  class  { B }
64, 5cun 3163 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1632 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3667  dfpr2  3669  ralprg  3695  rexprg  3696  prcom  3718  preq1  3719  qdass  3739  qdassr  3740  tpidm12  3741  prprc1  3749  difprsn1  3770  diftpsn3  3772  snsspr1  3780  snsspr2  3781  prss  3785  prssg  3786  ssunpr  3792  sstp  3794  pwssun  4315  xpsspw  4813  xpsspwOLD  4814  dmpropg  5162  funprg  5317  funtp  5319  f1oprswap  5531  fnimapr  5599  fpr  5720  fvpr1  5738  df2o3  6508  map2xp  7047  1sdom  7081  en2  7110  prfi  7147  prwf  7499  rankprb  7539  pr2nelem  7650  xp2cda  7822  ssxr  8908  prunioo  10780  hashprg  11384  hashprlei  11395  isprm2lem  12781  strlemor2  13252  strle2  13256  phlstr  13303  xpscg  13476  dmdprdpr  15300  dprdpr  15301  lsmpr  15858  lsppr  15862  lspsntri  15866  lsppratlem1  15916  lsppratlem3  15918  lsppratlem4  15919  xpstopnlem1  17516  ovolioo  18941  uniiccdif  18949  i1f1  19061  wilthlem2  20323  perfectlem2  20485  ex-dif  20826  ex-un  20827  ex-in  20828  ex-xp  20839  ex-cnv  20840  ex-rn  20843  ex-res  20844  spanpr  22175  superpos  22950  sumpr  23184  rnpropg  23205  fmptpr  23229  prct  23355  esumpr  23453  subfacp1lem1  23725  altopthsn  24567  axlowdimlem13  24654  onint1  24960  pgapspf  26155  smprngopr  26780  sumpair  27809  tpprceq3  28182  disjpr2  28185  f1oprg  28186  f1oun2prg  28187  s2prop  28221  s4prop  28222  constr3lem4  28393  constr3pthlem1  28401  constr3pthlem2  28402  dihprrnlem1N  32236  dihprrnlem2  32237  djhlsmat  32239  lclkrlem2c  32321  lclkrlem2v  32340  lcfrlem18  32372
  Copyright terms: Public domain W3C validator