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 4213
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 27417). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4299. For a more traditional definition, but requiring a dummy variable, see dfpr2 4228. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4223). 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 4212 . 2 class {𝐴, 𝐵}
41csn 4210 . . 3 class {𝐴}
52csn 4210 . . 3 class {𝐵}
64, 5cun 3605 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1523 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  4223  dfpr2  4228  ralprg  4266  rexprg  4267  csbprg  4276  disjpr2  4280  disjpr2OLD  4281  prcom  4299  preq1  4300  qdass  4320  qdassr  4321  tpidm12  4322  prprc1  4332  difprsn1  4362  diftpsn3OLD  4365  difpr  4366  tpprceq3  4367  snsspr1  4377  snsspr2  4378  prssg  4382  prssOLD  4384  ssunpr  4397  sstp  4399  iunxprg  4639  iunopeqop  5010  pwssun  5049  xpsspw  5266  dmpropg  5644  rnpropg  5651  funprg  5978  funprgOLD  5979  funtp  5983  fntpg  5986  funcnvpr  5988  f1oprswap  6218  f1oprg  6219  fnimapr  6301  residpr  6449  fpr  6461  fmptpr  6479  fvpr1  6497  fvpr1g  6499  fvpr2g  6500  df2o3  7618  map2xp  8171  1sdom  8204  en2  8237  prfi  8276  prwf  8712  rankprb  8752  pr2nelem  8865  xp2cda  9040  ssxr  10145  prunioo  12339  prinfzo0  12546  fzosplitpr  12617  hashprg  13220  hashprgOLD  13221  hashprlei  13288  s2prop  13698  s4prop  13701  f1oun2prg  13708  sumpr  14521  strlemor2OLD  16017  strle2  16021  phlstr  16081  xpscg  16265  symg2bas  17864  dmdprdpr  18494  dprdpr  18495  lsmpr  19137  lsppr  19141  lspsntri  19145  lsppratlem1  19195  lsppratlem3  19197  lsppratlem4  19198  m2detleib  20485  xpstopnlem1  21660  ovolioo  23382  uniiccdif  23392  i1f1  23502  wilthlem2  24840  perfectlem2  25000  axlowdimlem13  25879  ex-dif  27410  ex-un  27411  ex-in  27412  ex-xp  27423  ex-cnv  27424  ex-rn  27427  ex-res  27428  spanpr  28567  superpos  29341  prct  29620  prodpr  29700  esumpr  30256  eulerpartgbij  30562  signswch  30766  prodfzo03  30809  subfacp1lem1  31287  altopthsn  32193  onint1  32573  poimirlem8  33547  poimirlem9  33548  poimirlem15  33554  smprngopr  33981  dihprrnlem1N  37030  dihprrnlem2  37031  djhlsmat  37033  lclkrlem2c  37115  lclkrlem2v  37134  lcfrlem18  37166  dfrcl4  38285  iunrelexp0  38311  corclrcl  38316  corcltrcl  38348  cotrclrcl  38351  sumpair  39508  rnfdmpr  41623  perfectALTVlem2  41956  xpprsng  42435  gsumpr  42464
  Copyright terms: Public domain W3C validator