Definition df-pr 4588

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 30409). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4692. For a more traditional definition, but requiring a dummy variable, see dfpr2 4606. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4598). 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 4592. 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 4587	. 2 class {𝐴, 𝐵}
4	1	csn 4585	. . 3 class {𝐴}
5	2	csn 4585	. . 3 class {𝐵}
6	4, 5	cun 3909	. 2 class ({𝐴} ∪ {𝐵})
7	3, 6	wceq 1540	1 wff {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})

This definition is referenced by:  dfsn2  4598  dfpr2  4606  ralprgf  4654  rexprgf  4655  ralprg  4656  csbprg  4669  disjpr2  4673  prcom  4692  preq1  4693  qdass  4713  qdassr  4714  tpidm12  4715  prprc1  4725  difprsn1  4760  difpr  4763  tpprceq3  4764  snsspr1  4774  snsspr2  4775  prssg  4779  ssunpr  4794  sstp  4796  iunxprg  5055  iunopeqop  5476  pwssun  5523  xpsspw  5763  dmpropg  6176  rnpropg  6183  funprg  6554  funtp  6557  fntpg  6560  funcnvpr  6562  f1oprswap  6826  f1oprg  6827  fnimapr  6926  xpprsng  7094  residpr  7097  fpr  7108  fmptpr  7128  fvpr1g  7146  f1ofvswap  7263  df2o3  8419  enpr2dOLD  8998  map2xp  9088  1sdomOLD  9172  en2  9202  prfiALT  9251  prwf  9740  rankprb  9780  pr2nelemOLD  9932  xp2dju  10106  ssxr  11219  prunioo  13418  prinfzo0  13635  fzosplitpr  13713  hashprg  14336  hashprlei  14409  s2prop  14849  s4prop  14852  f1oun2prg  14859  s2rn  14905  sumpr  15690  strle2  17105  phlstr  17285  symg2bas  19307  gsumpr  19869  dmdprdpr  19965  dprdpr  19966  lsmpr  21028  lsppr  21032  lspsntri  21036  lsppratlem1  21089  lsppratlem3  21091  lsppratlem4  21092  m2detleib  22551  xpstopnlem1  23729  ovolioo  25502  uniiccdif  25512  i1f1  25624  wilthlem2  27012  perfectlem2  27174  axlowdimlem13  28934  ex-dif  30402  ex-un  30403  ex-in  30404  ex-xp  30415  ex-cnv  30416  ex-rn  30419  ex-res  30420  spanpr  31559  superpos  32333  cnvprop  32669  brprop  32670  mptprop  32671  coprprop  32672  prct  32688  prodpr  32801  ccfldextdgrr  33660  esumpr  34049  eulerpartgbij  34356  signswch  34545  prodfzo03  34587  subfacp1lem1  35159  altopthsn  35942  onint1  36430  bj-prexg  37020  bj-prex  37021  bj-prfromadj  37026  poimirlem8  37615  poimirlem9  37616  poimirlem15  37622  smprngopr  38039  dihprrnlem1N  41411  dihprrnlem2  41412  djhlsmat  41414  lclkrlem2c  41496  lclkrlem2v  41515  lcfrlem18  41547  pr2dom  43509  dfrcl4  43658  iunrelexp0  43684  corclrcl  43689  corcltrcl  43721  cotrclrcl  43724  mnuprdlem2  44255  sumpair  45022  rnfdmpr  47275  perfectALTVlem2  47716  usgrexmpl2edg  48013