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

Definition df-pr 3823
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 21740). They are unordered, so  { A ,  B }  =  { B ,  A } as proven by prcom 3884. For a more traditional definition, but requiring a dummy variable, see dfpr2 3832. (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 3817 . 2  class  { A ,  B }
41csn 3816 . . 3  class  { A }
52csn 3816 . . 3  class  { B }
64, 5cun 3320 . 2  class  ( { A }  u.  { B } )
73, 6wceq 1653 1  wff  { A ,  B }  =  ( { A }  u.  { B } )
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3830  dfpr2  3832  ralprg  3859  rexprg  3860  disjpr2  3872  prcom  3884  preq1  3885  qdass  3905  qdassr  3906  tpidm12  3907  prprc1  3916  difprsn1  3937  diftpsn3  3939  tpprceq3  3940  snsspr1  3949  snsspr2  3950  prss  3954  prssg  3955  ssunpr  3963  sstp  3965  pwssun  4491  xpsspw  4988  xpsspwOLD  4989  dmpropg  5345  funprg  5502  funtp  5505  fntpg  5508  f1oprswap  5719  f1oprg  5720  fnimapr  5789  fpr  5916  fvpr1  5937  fvpr1g  5939  fvpr2g  5940  df2o3  6739  map2xp  7279  1sdom  7313  en2  7346  prfi  7383  prwf  7739  rankprb  7779  pr2nelem  7890  xp2cda  8062  ssxr  9147  prunioo  11027  hashprg  11668  hashprlei  11688  s2prop  11863  s4prop  11864  f1oun2prg  11866  isprm2lem  13088  strlemor2  13559  strle2  13563  phlstr  13610  xpscg  13785  dmdprdpr  15609  dprdpr  15610  lsmpr  16163  lsppr  16167  lspsntri  16171  lsppratlem1  16221  lsppratlem3  16223  lsppratlem4  16224  xpstopnlem1  17843  ovolioo  19464  uniiccdif  19472  i1f1  19584  wilthlem2  20854  perfectlem2  21016  constr2spthlem1  21596  constr3pthlem1  21644  constr3pthlem2  21645  ex-dif  21733  ex-un  21734  ex-in  21735  ex-xp  21746  ex-cnv  21747  ex-rn  21750  ex-res  21751  spanpr  23084  superpos  23859  rnpropg  24037  fmptpr  24064  prct  24106  sumpr  24220  esumpr  24459  subfacp1lem1  24867  altopthsn  25808  axlowdimlem13  25895  onint1  26201  smprngopr  26664  sumpair  27684  difpr  28062  iunxprg  28071  rnfdmpr  28089  dihprrnlem1N  32284  dihprrnlem2  32285  djhlsmat  32287  lclkrlem2c  32369  lclkrlem2v  32388  lcfrlem18  32420
  Copyright terms: Public domain W3C validator