Definition df-pr 4591

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

This definition is used by:  dfsn2  4597  dfpr2  4605  ralprgf  4655  rexprgf  4656  ralprg  4657  csbprg  4670  disjpr2  4674  prcom  4693  preq1  4694  qdass  4714  qdassr  4715  tpidm12  4716  prprc1  4726  difprsn1  4763  difpr  4766  tpprceq3  4767  snsspr1  4773  snsspr2  4774  prssg  4778  ssunpr  4792  sstp  4794  iunxprg  5059  iunopeqop  5498  iunopeqopOLD  5499  pwssun  5547  xpsspw  5792  dmpropg  6228  rnpropg  6235  funprg  6613  funtp  6616  fntpg  6619  funcnvpr  6621  f1oprswap  6890  f1oprg  6891  fnimapr  6988  xpprsng  7163  xpsnprg  7164  xpsntpg  7165  residpr  7167  fpr  7179  fmptpr  7197  fvpr1g  7215  f1ofvswap  7334  df2o3  8509  map2xp  9191  en2  9296  prfiALT  9341  prwf  9843  rankprb  9889  xp2dju  10279  ssxr  11403  prunioo  13636  prinfzo0  13857  fzosplitpr  13936  hashprg  14563  hashprlei  14637  s2prop  15084  s4prop  15087  f1oun2prg  15094  s2rn  15142  sumpr  15940  strle2  17363  phlstr  17543  symg2bas  19634  gsumpr  20196  dmdprdpr  20292  dprdpr  20293  lsmpr  21391  lsppr  21395  lspsntri  21399  lsppratlem1  21452  lsppratlem3  21454  lsppratlem4  21455  m2detleib  22973  xpstopnlem1  24155  ovolioo  25916  uniiccdif  25926  i1f1  26038  wilthlem2  27423  perfectlem2  27584  bdaypw2n0bndlem  28876  axlowdimlem13  29559  ex-dif  31051  ex-un  31052  ex-in  31053  ex-xp  31064  ex-cnv  31065  ex-rn  31068  ex-res  31069  spanpr  32209  superpos  32983  cnvprop  33357  brprop  33358  mptprop  33359  coprprop  33360  prct  33374  prodpr  33484  ccfldextdgrr  34371  esumpr  34765  eulerpartgbij  35071  signswch  35257  prodfzo03  35299  subfacp1lem1  36110  altopthsn  36903  onint1  37414  bj-prexg  38129  bj-prex  38130  bj-prfromadj  38135  poimirlem8  38737  poimirlem9  38738  poimirlem15  38744  smprngopr  39177  dihprrnlem1N  42672  dihprrnlem2  42673  djhlsmat  42675  lclkrlem2c  42757  lclkrlem2v  42776  lcfrlem18  42808  pr2dom  44718  dfrcl4  44866  iunrelexp0  44892  corclrcl  44897  corcltrcl  44929  cotrclrcl  44932  mnuprdlem2  45447  relpropg  46111  hfpr  46209  sumpair  46255  rnfdmpr  48554  perfectALTVlem2  49023  usgrexmpl2edg  49330  smprngprmrng  49639