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

Definition df-pr 3551
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 20630). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3609. For a more traditional definition, but requiring a dummy variable, see dfpr2 3560. (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 3545 . 2  class  { A ,  B }
41csn 3544 . . 3  class  { A }
52csn 3544 . . 3  class  { B }
64, 5cun 3076 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1619 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3558  dfpr2  3560  ralprg  3586  rexprg  3587  prcom  3609  preq1  3610  qdass  3630  qdassr  3631  tpidm12  3632  prprc1  3640  snsspr1  3664  snsspr2  3665  prss  3669  prssg  3670  ssunpr  3676  sstp  3678  pwssun  4192  xpsspw  4704  xpsspwOLD  4705  dmpropg  5052  funprg  5158  funtp  5160  f1oprswap  5372  fnimapr  5435  fpr  5556  fvpr1  5574  df2o3  6378  map2xp  6916  1sdom  6950  en2  6979  prfi  7016  prwf  7367  rankprb  7407  pr2nelem  7518  xp2cda  7690  ssxr  8772  prunioo  10642  hashprg  11245  hashprlei  11256  isprm2lem  12639  strlemor2  13110  strle2  13114  phlstr  13161  xpscg  13334  dmdprdpr  15119  dprdpr  15120  lsmpr  15677  lsppr  15681  lspsntri  15685  lsppratlem1  15734  lsppratlem3  15736  lsppratlem4  15737  xpstopnlem1  17332  ovolioo  18757  uniiccdif  18765  i1f1  18877  wilthlem2  20139  perfectlem2  20301  ex-dif  20623  ex-un  20624  ex-in  20625  ex-xp  20636  ex-cnv  20637  ex-rn  20640  ex-res  20641  spanpr  21989  superpos  22764  subfacp1lem1  22881  altopthsn  23669  axlowdimlem13  23756  onint1  24062  repfuntw  24326  pgapspf  25218  smprngopr  25843  sumpair  26873  dihprrnlem1N  30518  dihprrnlem2  30519  djhlsmat  30521  lclkrlem2c  30603  lclkrlem2v  30622  lcfrlem18  30654
  Copyright terms: Public domain W3C validator