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 4373
Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 27614). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4458. For a more traditional definition, but requiring a dummy variable, see dfpr2 4389. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4383). 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 4372 . 2 class {𝐴, 𝐵}
41csn 4370 . . 3 class {𝐴}
52csn 4370 . . 3 class {𝐵}
64, 5cun 3767 . 2 class ({𝐴} ∪ {𝐵})
73, 6wceq 1637 1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
Colors of variables: wff setvar class
This definition is referenced by:  dfsn2  4383  dfpr2  4389  ralprg  4426  rexprg  4427  csbprg  4436  disjpr2  4440  prcom  4458  preq1  4459  qdass  4479  qdassr  4480  tpidm12  4481  prprc1  4491  difprsn1  4521  difpr  4524  tpprceq3  4525  snsspr1  4535  snsspr2  4536  prssg  4540  ssunpr  4553  sstp  4555  iunxprg  4799  iunopeqop  5176  pwssun  5215  xpsspw  5434  dmpropg  5820  rnpropg  5827  funprg  6150  funtp  6153  fntpg  6156  funcnvpr  6158  f1oprswap  6392  f1oprg  6393  fnimapr  6479  residpr  6628  fpr  6641  fmptpr  6659  fvpr1  6677  fvpr1g  6679  fvpr2g  6680  df2o3  7806  map2xp  8365  1sdom  8398  en2  8431  prfi  8470  prwf  8917  rankprb  8957  pr2nelem  9106  xp2cda  9283  ssxr  10388  prunioo  12520  prinfzo0  12727  fzosplitpr  12797  hashprg  13396  hashprlei  13463  s2prop  13872  s4prop  13875  f1oun2prg  13882  sumpr  14696  strlemor2OLD  16177  strle2  16181  phlstr  16241  xpscg  16419  symg2bas  18015  dmdprdpr  18646  dprdpr  18647  lsmpr  19292  lsppr  19296  lspsntri  19300  lsppratlem1  19352  lsppratlem3  19354  lsppratlem4  19355  m2detleib  20644  xpstopnlem1  21822  ovolioo  23545  uniiccdif  23555  i1f1  23667  wilthlem2  25005  perfectlem2  25165  axlowdimlem13  26044  ex-dif  27607  ex-un  27608  ex-in  27609  ex-xp  27620  ex-cnv  27621  ex-rn  27624  ex-res  27625  spanpr  28763  superpos  29537  prct  29815  prodpr  29895  esumpr  30449  eulerpartgbij  30755  signswch  30959  prodfzo03  31002  subfacp1lem1  31479  altopthsn  32384  onint1  32760  poimirlem8  33725  poimirlem9  33726  poimirlem15  33732  smprngopr  34157  dihprrnlem1N  37199  dihprrnlem2  37200  djhlsmat  37202  lclkrlem2c  37284  lclkrlem2v  37303  lcfrlem18  37335  dfrcl4  38462  iunrelexp0  38488  corclrcl  38493  corcltrcl  38525  cotrclrcl  38528  sumpair  39682  rnfdmpr  41865  perfectALTVlem2  42200  xpprsng  42672  gsumpr  42701
  Copyright terms: Public domain W3C validator