Definition df-pr 4604

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

This definition is referenced by:  dfsn2  4614  dfpr2  4622  ralprgf  4670  rexprgf  4671  ralprg  4672  csbprg  4685  disjpr2  4689  prcom  4708  preq1  4709  qdass  4729  qdassr  4730  tpidm12  4731  prprc1  4741  difprsn1  4776  difpr  4779  tpprceq3  4780  snsspr1  4790  snsspr2  4791  prssg  4795  ssunpr  4810  sstp  4812  iunxprg  5072  iunopeqop  5496  pwssun  5545  xpsspw  5788  dmpropg  6204  rnpropg  6211  funprg  6589  funtp  6592  fntpg  6595  funcnvpr  6597  f1oprswap  6861  f1oprg  6862  fnimapr  6961  xpprsng  7129  residpr  7132  fpr  7143  fmptpr  7163  fvpr1g  7181  f1ofvswap  7298  df2o3  8486  enpr2dOLD  9062  map2xp  9159  1sdomOLD  9255  en2  9285  prfiALT  9334  prwf  9823  rankprb  9863  pr2nelemOLD  10015  xp2dju  10189  ssxr  11302  prunioo  13496  prinfzo0  13713  fzosplitpr  13790  hashprg  14411  hashprlei  14484  s2prop  14924  s4prop  14927  f1oun2prg  14934  s2rn  14980  sumpr  15762  strle2  17176  phlstr  17358  symg2bas  19372  gsumpr  19934  dmdprdpr  20030  dprdpr  20031  lsmpr  21045  lsppr  21049  lspsntri  21053  lsppratlem1  21106  lsppratlem3  21108  lsppratlem4  21109  m2detleib  22567  xpstopnlem1  23745  ovolioo  25519  uniiccdif  25529  i1f1  25641  wilthlem2  27029  perfectlem2  27191  axlowdimlem13  28879  ex-dif  30350  ex-un  30351  ex-in  30352  ex-xp  30363  ex-cnv  30364  ex-rn  30367  ex-res  30368  spanpr  31507  superpos  32281  cnvprop  32619  brprop  32620  mptprop  32621  coprprop  32622  prct  32638  prodpr  32751  ccfldextdgrr  33659  esumpr  34043  eulerpartgbij  34350  signswch  34539  prodfzo03  34581  subfacp1lem1  35147  altopthsn  35925  onint1  36413  bj-prexg  37003  bj-prex  37004  bj-prfromadj  37009  poimirlem8  37598  poimirlem9  37599  poimirlem15  37605  smprngopr  38022  dihprrnlem1N  41389  dihprrnlem2  41390  djhlsmat  41392  lclkrlem2c  41474  lclkrlem2v  41493  lcfrlem18  41525  pr2dom  43498  dfrcl4  43647  iunrelexp0  43673  corclrcl  43678  corcltrcl  43710  cotrclrcl  43713  mnuprdlem2  44245  sumpair  45007  rnfdmpr  47258  perfectALTVlem2  47684  usgrexmpl2edg  47981