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 4531
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 28219). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4631. For a more traditional definition, but requiring a dummy variable, see dfpr2 4547. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4541). Therefore, {𝐴, 𝐵} is called a proper (unordered) pair iff 𝐴𝐵 and 𝐴 and 𝐵 are sets.

Note: ordered pairs are a completely different object defined below in df-op 4535. When the term "pair" is used without qualifier, it generally means "unordered pair", and the context makes it clear which version is meant. (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 4530 . 2 class {𝐴, 𝐵}
41csn 4528 . . 3 class {𝐴}
52csn 4528 . . 3 class {𝐵}
64, 5cun 3882 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1538 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  4541  dfpr2  4547  ralprgf  4593  rexprgf  4594  csbprg  4608  disjpr2  4612  prcom  4631  preq1  4632  qdass  4652  qdassr  4653  tpidm12  4654  prprc1  4664  difprsn1  4696  difpr  4699  tpprceq3  4700  snsspr1  4710  snsspr2  4711  prssg  4715  ssunpr  4728  sstp  4730  iunxprg  4984  iunopeqop  5379  pwssun  5424  xpsspw  5650  dmpropg  6043  rnpropg  6050  funprg  6382  funtp  6385  fntpg  6388  funcnvpr  6390  f1oprswap  6637  f1oprg  6638  fnimapr  6726  xpprsng  6883  residpr  6886  fpr  6897  fmptpr  6915  fvpr1  6933  fvpr1g  6935  fvpr2g  6936  df2o3  8104  enpr2d  8584  map2xp  8675  1sdom  8709  en2  8742  prfi  8781  prwf  9228  rankprb  9268  pr2nelem  9419  xp2dju  9591  ssxr  10703  prunioo  12863  prinfzo0  13075  fzosplitpr  13145  hashprg  13756  hashprlei  13826  s2prop  14264  s4prop  14267  f1oun2prg  14274  sumpr  15099  strle2  16589  phlstr  16649  symg2bas  18517  gsumpr  19072  dmdprdpr  19168  dprdpr  19169  lsmpr  19858  lsppr  19862  lspsntri  19866  lsppratlem1  19916  lsppratlem3  19918  lsppratlem4  19919  m2detleib  21240  xpstopnlem1  22418  ovolioo  24176  uniiccdif  24186  i1f1  24298  wilthlem2  25658  perfectlem2  25818  axlowdimlem13  26752  ex-dif  28212  ex-un  28213  ex-in  28214  ex-xp  28225  ex-cnv  28226  ex-rn  28229  ex-res  28230  spanpr  29367  superpos  30141  cnvprop  30460  brprop  30461  mptprop  30462  coprprop  30463  prct  30480  prodpr  30572  ccfldextdgrr  31149  esumpr  31439  eulerpartgbij  31744  signswch  31945  prodfzo03  31988  subfacp1lem1  32540  altopthsn  33536  onint1  33911  poimirlem8  35064  poimirlem9  35065  poimirlem15  35071  smprngopr  35489  dihprrnlem1N  38719  dihprrnlem2  38720  djhlsmat  38722  lclkrlem2c  38804  lclkrlem2v  38823  lcfrlem18  38855  pr2dom  40228  dfrcl4  40370  iunrelexp0  40396  corclrcl  40401  corcltrcl  40433  cotrclrcl  40436  mnuprdlem2  40974  sumpair  41657  rnfdmpr  43830  perfectALTVlem2  44233
  Copyright terms: Public domain W3C validator