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

Definition df-pr 3785
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 21695). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3846. For a more traditional definition, but requiring a dummy variable, see dfpr2 3794. (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 3779 . 2  class  { A ,  B }
41csn 3778 . . 3  class  { A }
52csn 3778 . . 3  class  { B }
64, 5cun 3282 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1649 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3792  dfpr2  3794  ralprg  3821  rexprg  3822  disjpr2  3834  prcom  3846  preq1  3847  qdass  3867  qdassr  3868  tpidm12  3869  prprc1  3878  difprsn1  3899  diftpsn3  3901  tpprceq3  3902  snsspr1  3911  snsspr2  3912  prss  3916  prssg  3917  ssunpr  3925  sstp  3927  pwssun  4453  xpsspw  4949  xpsspwOLD  4950  dmpropg  5306  funprg  5463  funtp  5466  fntpg  5469  f1oprswap  5680  f1oprg  5681  fnimapr  5750  fpr  5877  fvpr1  5898  fvpr1g  5900  fvpr2g  5901  df2o3  6700  map2xp  7240  1sdom  7274  en2  7307  prfi  7344  prwf  7697  rankprb  7737  pr2nelem  7848  xp2cda  8020  ssxr  9105  prunioo  10985  hashprg  11625  hashprlei  11645  s2prop  11820  s4prop  11821  f1oun2prg  11823  isprm2lem  13045  strlemor2  13516  strle2  13520  phlstr  13567  xpscg  13742  dmdprdpr  15566  dprdpr  15567  lsmpr  16120  lsppr  16124  lspsntri  16128  lsppratlem1  16178  lsppratlem3  16180  lsppratlem4  16181  xpstopnlem1  17798  ovolioo  19419  uniiccdif  19427  i1f1  19539  wilthlem2  20809  perfectlem2  20971  constr2spthlem1  21551  constr3pthlem1  21599  constr3pthlem2  21600  ex-dif  21688  ex-un  21689  ex-in  21690  ex-xp  21701  ex-cnv  21702  ex-rn  21705  ex-res  21706  spanpr  23039  superpos  23814  rnpropg  23992  fmptpr  24019  prct  24061  sumpr  24175  esumpr  24414  subfacp1lem1  24822  altopthsn  25714  axlowdimlem13  25801  onint1  26107  smprngopr  26556  sumpair  27577  iunxprg  27960  rnfdmpr  27968  dihprrnlem1N  31911  dihprrnlem2  31912  djhlsmat  31914  lclkrlem2c  31996  lclkrlem2v  32015  lcfrlem18  32047
  Copyright terms: Public domain W3C validator