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

Definition df-pr 3781
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 21691). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3842. For a more traditional definition, but requiring a dummy variable, see dfpr2 3790. (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 3775 . 2  class  { A ,  B }
41csn 3774 . . 3  class  { A }
52csn 3774 . . 3  class  { B }
64, 5cun 3278 . 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  3788  dfpr2  3790  ralprg  3817  rexprg  3818  disjpr2  3830  prcom  3842  preq1  3843  qdass  3863  qdassr  3864  tpidm12  3865  prprc1  3874  difprsn1  3895  diftpsn3  3897  tpprceq3  3898  snsspr1  3907  snsspr2  3908  prss  3912  prssg  3913  ssunpr  3921  sstp  3923  pwssun  4449  xpsspw  4945  xpsspwOLD  4946  dmpropg  5302  funprg  5459  funtp  5462  fntpg  5465  f1oprswap  5676  f1oprg  5677  fnimapr  5746  fpr  5873  fvpr1  5894  fvpr1g  5896  fvpr2g  5897  df2o3  6696  map2xp  7236  1sdom  7270  en2  7303  prfi  7340  prwf  7693  rankprb  7733  pr2nelem  7844  xp2cda  8016  ssxr  9101  prunioo  10981  hashprg  11621  hashprlei  11641  s2prop  11816  s4prop  11817  f1oun2prg  11819  isprm2lem  13041  strlemor2  13512  strle2  13516  phlstr  13563  xpscg  13738  dmdprdpr  15562  dprdpr  15563  lsmpr  16116  lsppr  16120  lspsntri  16124  lsppratlem1  16174  lsppratlem3  16176  lsppratlem4  16177  xpstopnlem1  17794  ovolioo  19415  uniiccdif  19423  i1f1  19535  wilthlem2  20805  perfectlem2  20967  constr2spthlem1  21547  constr3pthlem1  21595  constr3pthlem2  21596  ex-dif  21684  ex-un  21685  ex-in  21686  ex-xp  21697  ex-cnv  21698  ex-rn  21701  ex-res  21702  spanpr  23035  superpos  23810  rnpropg  23988  fmptpr  24015  prct  24057  sumpr  24171  esumpr  24410  subfacp1lem1  24818  altopthsn  25710  axlowdimlem13  25797  onint1  26103  smprngopr  26552  sumpair  27573  iunxprg  27956  rnfdmpr  27964  dihprrnlem1N  31907  dihprrnlem2  31908  djhlsmat  31910  lclkrlem2c  31992  lclkrlem2v  32011  lcfrlem18  32043
  Copyright terms: Public domain W3C validator