Definition df-pr 4561

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 28695). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4665. For a more traditional definition, but requiring a dummy variable, see dfpr2 4577. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4571). 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 4565. 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cpr 4560	. 2 class {𝐴, 𝐵}
4	1	csn 4558	. . 3 class {𝐴}
5	2	csn 4558	. . 3 class {𝐵}
6	4, 5	cun 3881	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1539	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  4571  dfpr2  4577  ralprgf  4625  rexprgf  4626  ralprg  4627  csbprg  4642  disjpr2  4646  prcom  4665  preq1  4666  qdass  4686  qdassr  4687  tpidm12  4688  prprc1  4698  difprsn1  4730  difpr  4733  tpprceq3  4734  snsspr1  4744  snsspr2  4745  prssg  4749  ssunpr  4762  sstp  4764  iunxprg  5021  iunopeqop  5429  pwssun  5476  xpsspw  5708  dmpropg  6107  rnpropg  6114  funprg  6472  funtp  6475  fntpg  6478  funcnvpr  6480  f1oprswap  6743  f1oprg  6744  fnimapr  6834  xpprsng  6994  residpr  6997  fpr  7008  fmptpr  7026  fvpr1g  7044  fvpr2gOLD  7046  fvpr1OLD  7048  f1ofvswap  7158  df2o3  8282  enpr2d  8792  map2xp  8883  1sdom  8955  en2  8983  prfi  9019  prwf  9500  rankprb  9540  pr2nelem  9691  xp2dju  9863  ssxr  10975  prunioo  13142  prinfzo0  13354  fzosplitpr  13424  hashprg  14038  hashprlei  14110  s2prop  14548  s4prop  14551  f1oun2prg  14558  sumpr  15388  strle2  16788  phlstr  16981  symg2bas  18915  gsumpr  19471  dmdprdpr  19567  dprdpr  19568  lsmpr  20266  lsppr  20270  lspsntri  20274  lsppratlem1  20324  lsppratlem3  20326  lsppratlem4  20327  m2detleib  21688  xpstopnlem1  22868  ovolioo  24637  uniiccdif  24647  i1f1  24759  wilthlem2  26123  perfectlem2  26283  axlowdimlem13  27225  ex-dif  28688  ex-un  28689  ex-in  28690  ex-xp  28701  ex-cnv  28702  ex-rn  28705  ex-res  28706  spanpr  29843  superpos  30617  cnvprop  30931  brprop  30932  mptprop  30933  coprprop  30934  prct  30951  prodpr  31042  ccfldextdgrr  31644  esumpr  31934  eulerpartgbij  32239  signswch  32440  prodfzo03  32483  subfacp1lem1  33041  altopthsn  34190  onint1  34565  poimirlem8  35712  poimirlem9  35713  poimirlem15  35719  smprngopr  36137  dihprrnlem1N  39365  dihprrnlem2  39366  djhlsmat  39368  lclkrlem2c  39450  lclkrlem2v  39469  lcfrlem18  39501  pr2dom  41032  dfrcl4  41173  iunrelexp0  41199  corclrcl  41204  corcltrcl  41236  cotrclrcl  41239  mnuprdlem2  41780  sumpair  42467  rnfdmpr  44660  perfectALTVlem2  45062