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

Definition df-pr 3848
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For ?Error: 1 , -u 1 } -> ( A ^ 2 ) = 1 ^ This math symbol is not active (i.e. was not declared in this scope). example, e.{1,-u1}->( 2)=1 (ex-pr 21789). They are unordered, so as proven by prcom 3910. For a more traditional definition, but requiring a dummy variable, see dfpr2 3857. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-pr

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cpr 3842 . 2
41csn 3841 . . 3
52csn 3841 . . 3
64, 5cun 3307 . 2
73, 6wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  dfsn2  3855  dfpr2  3857  ralprg  3885  rexprg  3886  disjpr2  3898  prcom  3910  preq1  3911  qdass  3931  qdassr  3932  tpidm12  3933  prprc1  3942  difprsn1  3963  diftpsn3  3965  tpprceq3  3966  snsspr1  3975  snsspr2  3976  prss  3980  prssg  3981  ssunpr  3989  sstp  3991  pwssun  4530  xpsspw  5028  xpsspwOLD  5029  dmpropg  5389  funprg  5547  funtp  5550  fntpg  5553  f1oprswap  5764  f1oprg  5765  fnimapr  5835  fpr  5962  fvpr1  5983  fvpr1g  5985  fvpr2g  5986  df2o3  6786  map2xp  7326  1sdom  7360  en2  7393  prfi  7430  prwf  7786  rankprb  7826  pr2nelem  7939  xp2cda  8111  ssxr  9196  prunioo  11076  hashprg  11717  hashprlei  11737  s2prop  11912  s4prop  11913  f1oun2prg  11915  isprm2lem  13137  strlemor2  13608  strle2  13612  phlstr  13659  xpscg  13834  dmdprdpr  15658  dprdpr  15659  lsmpr  16212  lsppr  16216  lspsntri  16220  lsppratlem1  16270  lsppratlem3  16272  lsppratlem4  16273  xpstopnlem1  17892  ovolioo  19513  uniiccdif  19521  i1f1  19631  wilthlem2  20903  perfectlem2  21065  constr2spthlem1  21645  constr3pthlem1  21693  constr3pthlem2  21694  ex-dif  21782  ex-un  21783  ex-in  21784  ex-xp  21795  ex-cnv  21796  ex-rn  21799  ex-res  21800  spanpr  23133  superpos  23908  rnpropg  24084  fmptpr  24110  prct  24152  sumpr  24267  esumpr  24506  eulerpartgbij  24758  subfacp1lem1  24969  altopthsn  25910  axlowdimlem13  25997  onint1  26303  smprngopr  26773  sumpair  27860  difpr  28239  iunxprg  28248  rnfdmpr  28265  dihprrnlem1N  32462  dihprrnlem2  32463  djhlsmat  32465  lclkrlem2c  32547  lclkrlem2v  32566  lcfrlem18  32598
  Copyright terms: Public domain W3C validator