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

Definition df-pr 3764
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 21586). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3825. For a more traditional definition, but requiring a dummy variable, see dfpr2 3773. (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 3758 . 2  class  { A ,  B }
41csn 3757 . . 3  class  { A }
52csn 3757 . . 3  class  { B }
64, 5cun 3261 . 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  3771  dfpr2  3773  ralprg  3800  rexprg  3801  disjpr2  3813  prcom  3825  preq1  3826  qdass  3846  qdassr  3847  tpidm12  3848  prprc1  3857  difprsn1  3878  diftpsn3  3880  tpprceq3  3881  snsspr1  3890  snsspr2  3891  prss  3895  prssg  3896  ssunpr  3904  sstp  3906  pwssun  4430  xpsspw  4926  xpsspwOLD  4927  dmpropg  5283  funprg  5440  funtp  5443  fntpg  5446  f1oprswap  5657  f1oprg  5658  fnimapr  5726  fpr  5853  fvpr1  5874  fvpr1g  5876  fvpr2g  5877  df2o3  6673  map2xp  7213  1sdom  7247  en2  7280  prfi  7317  prwf  7670  rankprb  7710  pr2nelem  7821  xp2cda  7993  ssxr  9078  prunioo  10957  hashprg  11593  hashprlei  11613  s2prop  11788  s4prop  11789  f1oun2prg  11791  isprm2lem  13013  strlemor2  13484  strle2  13488  phlstr  13535  xpscg  13710  dmdprdpr  15534  dprdpr  15535  lsmpr  16088  lsppr  16092  lspsntri  16096  lsppratlem1  16146  lsppratlem3  16148  lsppratlem4  16149  xpstopnlem1  17762  ovolioo  19329  uniiccdif  19337  i1f1  19449  wilthlem2  20719  perfectlem2  20881  constr3pthlem1  21490  constr3pthlem2  21491  ex-dif  21579  ex-un  21580  ex-in  21581  ex-xp  21592  ex-cnv  21593  ex-rn  21596  ex-res  21597  spanpr  22930  superpos  23705  rnpropg  23878  fmptpr  23904  prct  23945  sumpr  24047  esumpr  24253  subfacp1lem1  24644  altopthsn  25520  axlowdimlem13  25607  onint1  25913  smprngopr  26353  sumpair  27374  dihprrnlem1N  31539  dihprrnlem2  31540  djhlsmat  31542  lclkrlem2c  31624  lclkrlem2v  31643  lcfrlem18  31675
  Copyright terms: Public domain W3C validator