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 4316
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 27590). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4403. For a more traditional definition, but requiring a dummy variable, see dfpr2 4331. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4326). Therefore, {𝐴, 𝐵} is called a proper (unordered) pair iff 𝐴𝐵 and 𝐴 and 𝐵 are sets. (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 4315 . 2 class {𝐴, 𝐵}
41csn 4313 . . 3 class {𝐴}
52csn 4313 . . 3 class {𝐵}
64, 5cun 3705 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1624 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  4326  dfpr2  4331  ralprg  4370  rexprg  4371  csbprg  4380  disjpr2  4384  disjpr2OLD  4385  prcom  4403  preq1  4404  qdass  4424  qdassr  4425  tpidm12  4426  prprc1  4436  difprsn1  4467  diftpsn3OLD  4470  difpr  4471  tpprceq3  4472  snsspr1  4482  snsspr2  4483  prssg  4487  prssOLD  4489  ssunpr  4502  sstp  4504  iunxprg  4751  iunopeqop  5123  pwssun  5162  xpsspw  5381  dmpropg  5759  rnpropg  5766  funprg  6093  funprgOLD  6094  funtp  6098  fntpg  6101  funcnvpr  6103  f1oprswap  6333  f1oprg  6334  fnimapr  6416  residpr  6564  fpr  6576  fmptpr  6594  fvpr1  6612  fvpr1g  6614  fvpr2g  6615  df2o3  7734  map2xp  8287  1sdom  8320  en2  8353  prfi  8392  prwf  8839  rankprb  8879  pr2nelem  9009  xp2cda  9186  ssxr  10291  prunioo  12486  prinfzo0  12693  fzosplitpr  12763  hashprg  13366  hashprgOLD  13367  hashprlei  13434  s2prop  13844  s4prop  13847  f1oun2prg  13854  sumpr  14668  strlemor2OLD  16164  strle2  16168  phlstr  16228  xpscg  16412  symg2bas  18010  dmdprdpr  18640  dprdpr  18641  lsmpr  19283  lsppr  19287  lspsntri  19291  lsppratlem1  19341  lsppratlem3  19343  lsppratlem4  19344  m2detleib  20631  xpstopnlem1  21806  ovolioo  23528  uniiccdif  23538  i1f1  23648  wilthlem2  24986  perfectlem2  25146  axlowdimlem13  26025  ex-dif  27583  ex-un  27584  ex-in  27585  ex-xp  27596  ex-cnv  27597  ex-rn  27600  ex-res  27601  spanpr  28740  superpos  29514  prct  29793  prodpr  29873  esumpr  30429  eulerpartgbij  30735  signswch  30939  prodfzo03  30982  subfacp1lem1  31460  altopthsn  32366  onint1  32746  poimirlem8  33722  poimirlem9  33723  poimirlem15  33729  smprngopr  34156  dihprrnlem1N  37207  dihprrnlem2  37208  djhlsmat  37210  lclkrlem2c  37292  lclkrlem2v  37311  lcfrlem18  37343  dfrcl4  38462  iunrelexp0  38488  corclrcl  38493  corcltrcl  38525  cotrclrcl  38528  sumpair  39685  rnfdmpr  41800  perfectALTVlem2  42133  xpprsng  42612  gsumpr  42641
  Copyright terms: Public domain W3C validator