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

Definition df-pr 3813
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 21730). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3874. For a more traditional definition, but requiring a dummy variable, see dfpr2 3822. (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 3807 . 2  class  { A ,  B }
41csn 3806 . . 3  class  { A }
52csn 3806 . . 3  class  { B }
64, 5cun 3310 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1652 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3820  dfpr2  3822  ralprg  3849  rexprg  3850  disjpr2  3862  prcom  3874  preq1  3875  qdass  3895  qdassr  3896  tpidm12  3897  prprc1  3906  difprsn1  3927  diftpsn3  3929  tpprceq3  3930  snsspr1  3939  snsspr2  3940  prss  3944  prssg  3945  ssunpr  3953  sstp  3955  pwssun  4481  xpsspw  4978  xpsspwOLD  4979  dmpropg  5335  funprg  5492  funtp  5495  fntpg  5498  f1oprswap  5709  f1oprg  5710  fnimapr  5779  fpr  5906  fvpr1  5927  fvpr1g  5929  fvpr2g  5930  df2o3  6729  map2xp  7269  1sdom  7303  en2  7336  prfi  7373  prwf  7729  rankprb  7769  pr2nelem  7880  xp2cda  8052  ssxr  9137  prunioo  11017  hashprg  11658  hashprlei  11678  s2prop  11853  s4prop  11854  f1oun2prg  11856  isprm2lem  13078  strlemor2  13549  strle2  13553  phlstr  13600  xpscg  13775  dmdprdpr  15599  dprdpr  15600  lsmpr  16153  lsppr  16157  lspsntri  16161  lsppratlem1  16211  lsppratlem3  16213  lsppratlem4  16214  xpstopnlem1  17833  ovolioo  19454  uniiccdif  19462  i1f1  19574  wilthlem2  20844  perfectlem2  21006  constr2spthlem1  21586  constr3pthlem1  21634  constr3pthlem2  21635  ex-dif  21723  ex-un  21724  ex-in  21725  ex-xp  21736  ex-cnv  21737  ex-rn  21740  ex-res  21741  spanpr  23074  superpos  23849  rnpropg  24027  fmptpr  24054  prct  24096  sumpr  24210  esumpr  24449  subfacp1lem1  24857  altopthsn  25798  axlowdimlem13  25885  onint1  26191  smprngopr  26653  sumpair  27673  iunxprg  28058  rnfdmpr  28069  dihprrnlem1N  32159  dihprrnlem2  32160  djhlsmat  32162  lclkrlem2c  32244  lclkrlem2v  32263  lcfrlem18  32295
  Copyright terms: Public domain W3C validator