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

Definition df-pr 4127
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 26472). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4210. For a more traditional definition, but requiring a dummy variable, see dfpr2 4142. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
df-pr {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

Detailed syntax breakdown of Definition df-pr
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cpr 4126 . 2 class {𝐴, 𝐵}
41csn 4124 . . 3 class {𝐴}
52csn 4124 . . 3 class {𝐵}
64, 5cun 3537 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1474 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  4137  dfpr2  4142  ralprg  4180  rexprg  4181  csbprg  4190  disjpr2  4193  disjpr2OLD  4194  prcom  4210  preq1  4211  qdass  4231  qdassr  4232  tpidm12  4233  prprc1  4242  difprsn1  4270  diftpsn3OLD  4273  difpr  4274  tpprceq3  4275  snsspr1  4284  snsspr2  4285  prssg  4289  prssOLD  4291  ssunpr  4300  sstp  4302  iunxprg  4537  pwssun  4933  xpsspw  5144  dmpropg  5511  rnpropg  5518  funprg  5839  funprgOLD  5840  funtp  5844  fntpg  5847  funcnvpr  5849  f1oprswap  6076  f1oprg  6077  fnimapr  6156  residpr  6299  fpr  6303  fmptpr  6320  fvpr1  6338  fvpr1g  6340  fvpr2g  6341  df2o3  7437  map2xp  7992  1sdom  8025  en2  8058  prfi  8097  prwf  8534  rankprb  8574  pr2nelem  8687  xp2cda  8862  ssxr  9958  prunioo  12130  fzosplitprm1  12400  hashprg  12997  hashprgOLD  12998  hashprlei  13061  s2prop  13450  s4prop  13453  f1oun2prg  13460  sumpr  14269  isprm2lem  15180  strlemor2  15745  strle2  15749  phlstr  15805  xpscg  15989  symg2bas  17589  dmdprdpr  18219  dprdpr  18220  lsmpr  18858  lsppr  18862  lspsntri  18866  lsppratlem1  18916  lsppratlem3  18918  lsppratlem4  18919  m2detleib  20203  xpstopnlem1  21369  ovolioo  23087  uniiccdif  23096  i1f1  23207  wilthlem2  24539  perfectlem2  24699  axlowdimlem13  25579  nbgraopALT  25746  constr2spthlem1  25917  constr3pthlem1  25976  constr3pthlem2  25977  ex-dif  26465  ex-un  26466  ex-in  26467  ex-xp  26478  ex-cnv  26479  ex-rn  26482  ex-res  26483  spanpr  27616  superpos  28390  prct  28668  esumpr  29248  eulerpartgbij  29554  signswch  29757  subfacp1lem1  30208  altopthsn  31031  onint1  31411  poimirlem8  32370  poimirlem9  32371  poimirlem15  32377  smprngopr  32804  dihprrnlem1N  35514  dihprrnlem2  35515  djhlsmat  35517  lclkrlem2c  35599  lclkrlem2v  35618  lcfrlem18  35650  dfrcl4  36770  iunrelexp0  36796  corclrcl  36801  corcltrcl  36833  cotrclrcl  36836  sumpair  38000  perfectALTVlem2  39949  iunopeqop  40110  rnfdmpr  40120  fzosplitpr  40168  prinfzo0  40169  xpprsng  41884  gsumpr  41913
  Copyright terms: Public domain W3C validator