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 4562
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 28137). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4662. For a more traditional definition, but requiring a dummy variable, see dfpr2 4578. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4572). 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 4561 . 2 class {𝐴, 𝐵}
41csn 4559 . . 3 class {𝐴}
52csn 4559 . . 3 class {𝐵}
64, 5cun 3933 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1528 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  4572  dfpr2  4578  ralprgf  4624  rexprgf  4625  csbprg  4639  disjpr2  4643  prcom  4662  preq1  4663  qdass  4683  qdassr  4684  tpidm12  4685  prprc1  4695  difprsn1  4727  difpr  4730  tpprceq3  4731  snsspr1  4741  snsspr2  4742  prssg  4746  ssunpr  4759  sstp  4761  iunxprg  5010  iunopeqop  5403  pwssun  5449  xpsspw  5676  dmpropg  6066  rnpropg  6073  funprg  6402  funtp  6405  fntpg  6408  funcnvpr  6410  f1oprswap  6652  f1oprg  6653  fnimapr  6741  xpprsng  6895  residpr  6898  fpr  6909  fmptpr  6927  fvpr1  6945  fvpr1g  6947  fvpr2g  6948  df2o3  8108  enpr2d  8586  map2xp  8676  1sdom  8710  en2  8743  prfi  8782  prwf  9229  rankprb  9269  pr2nelem  9419  xp2dju  9591  ssxr  10699  prunioo  12857  prinfzo0  13066  fzosplitpr  13136  hashprg  13746  hashprlei  13816  s2prop  14259  s4prop  14262  f1oun2prg  14269  sumpr  15093  strle2  16583  phlstr  16643  symg2bas  18457  gsumpr  19006  dmdprdpr  19102  dprdpr  19103  lsmpr  19792  lsppr  19796  lspsntri  19800  lsppratlem1  19850  lsppratlem3  19852  lsppratlem4  19853  m2detleib  21170  xpstopnlem1  22347  ovolioo  24098  uniiccdif  24108  i1f1  24220  wilthlem2  25574  perfectlem2  25734  axlowdimlem13  26668  ex-dif  28130  ex-un  28131  ex-in  28132  ex-xp  28143  ex-cnv  28144  ex-rn  28147  ex-res  28148  spanpr  29285  superpos  30059  cnvprop  30359  brprop  30360  mptprop  30361  coprprop  30362  prct  30377  prodpr  30470  ccfldextdgrr  30957  esumpr  31225  eulerpartgbij  31530  signswch  31731  prodfzo03  31774  subfacp1lem1  32324  altopthsn  33320  onint1  33695  poimirlem8  34782  poimirlem9  34783  poimirlem15  34789  smprngopr  35213  dihprrnlem1N  38442  dihprrnlem2  38443  djhlsmat  38445  lclkrlem2c  38527  lclkrlem2v  38546  lcfrlem18  38578  pr2dom  39773  dfrcl4  39901  iunrelexp0  39927  corclrcl  39932  corcltrcl  39964  cotrclrcl  39967  mnuprdlem2  40489  sumpair  41172  rnfdmpr  43361  perfectALTVlem2  43734
  Copyright terms: Public domain W3C validator