Definition df-pr 4592

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

This definition is referenced by:  dfsn2  4602  dfpr2  4610  ralprgf  4658  rexprgf  4659  ralprg  4660  csbprg  4673  disjpr2  4677  prcom  4696  preq1  4697  qdass  4717  qdassr  4718  tpidm12  4719  prprc1  4729  difprsn1  4764  difpr  4767  tpprceq3  4768  snsspr1  4778  snsspr2  4779  prssg  4783  ssunpr  4798  sstp  4800  iunxprg  5060  iunopeqop  5481  pwssun  5530  xpsspw  5772  dmpropg  6188  rnpropg  6195  funprg  6570  funtp  6573  fntpg  6576  funcnvpr  6578  f1oprswap  6844  f1oprg  6845  fnimapr  6944  xpprsng  7112  residpr  7115  fpr  7126  fmptpr  7146  fvpr1g  7164  f1ofvswap  7281  df2o3  8442  enpr2dOLD  9021  map2xp  9111  1sdomOLD  9196  en2  9226  prfiALT  9275  prwf  9764  rankprb  9804  pr2nelemOLD  9956  xp2dju  10130  ssxr  11243  prunioo  13442  prinfzo0  13659  fzosplitpr  13737  hashprg  14360  hashprlei  14433  s2prop  14873  s4prop  14876  f1oun2prg  14883  s2rn  14929  sumpr  15714  strle2  17129  phlstr  17309  symg2bas  19323  gsumpr  19885  dmdprdpr  19981  dprdpr  19982  lsmpr  20996  lsppr  21000  lspsntri  21004  lsppratlem1  21057  lsppratlem3  21059  lsppratlem4  21060  m2detleib  22518  xpstopnlem1  23696  ovolioo  25469  uniiccdif  25479  i1f1  25591  wilthlem2  26979  perfectlem2  27141  axlowdimlem13  28881  ex-dif  30352  ex-un  30353  ex-in  30354  ex-xp  30365  ex-cnv  30366  ex-rn  30369  ex-res  30370  spanpr  31509  superpos  32283  cnvprop  32619  brprop  32620  mptprop  32621  coprprop  32622  prct  32638  prodpr  32751  ccfldextdgrr  33667  esumpr  34056  eulerpartgbij  34363  signswch  34552  prodfzo03  34594  subfacp1lem1  35166  altopthsn  35949  onint1  36437  bj-prexg  37027  bj-prex  37028  bj-prfromadj  37033  poimirlem8  37622  poimirlem9  37623  poimirlem15  37629  smprngopr  38046  dihprrnlem1N  41418  dihprrnlem2  41419  djhlsmat  41421  lclkrlem2c  41503  lclkrlem2v  41522  lcfrlem18  41554  pr2dom  43516  dfrcl4  43665  iunrelexp0  43691  corclrcl  43696  corcltrcl  43728  cotrclrcl  43731  mnuprdlem2  44262  sumpair  45029  rnfdmpr  47279  perfectALTVlem2  47720  usgrexmpl2edg  48017