Definition df-pr 4560

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

This definition is referenced by:  dfsn2  4570  dfpr2  4578  ralprgf  4628  rexprgf  4629  ralprg  4630  csbprg  4643  disjpr2  4647  prcom  4666  preq1  4667  qdass  4687  qdassr  4688  tpidm12  4689  prprc1  4699  difprsn1  4735  difpr  4738  tpprceq3  4739  snsspr1  4747  snsspr2  4748  prssg  4752  ssunpr  4767  sstp  4769  iunxprg  5027  iunopeqop  5464  iunopeqopOLD  5465  pwssun  5512  xpsspw  5754  dmpropg  6168  rnpropg  6175  funprg  6541  funtp  6544  fntpg  6547  funcnvpr  6549  f1oprswap  6814  f1oprg  6815  fnimapr  6912  xpprsng  7082  residpr  7085  fpr  7097  fmptpr  7116  fvpr1g  7134  f1ofvswap  7250  df2o3  8402  map2xp  9074  en2  9179  prfiALT  9224  prwf  9724  rankprb  9764  xp2dju  10088  ssxr  11204  prunioo  13423  prinfzo0  13642  fzosplitpr  13721  hashprg  14346  hashprlei  14419  s2prop  14858  s4prop  14861  f1oun2prg  14868  s2rn  14914  sumpr  15699  strle2  17118  phlstr  17298  symg2bas  19357  gsumpr  19919  dmdprdpr  20015  dprdpr  20016  lsmpr  21073  lsppr  21077  lspsntri  21081  lsppratlem1  21134  lsppratlem3  21136  lsppratlem4  21137  m2detleib  22584  xpstopnlem1  23762  ovolioo  25523  uniiccdif  25533  i1f1  25645  wilthlem2  27020  perfectlem2  27181  bdaypw2n0bndlem  28443  axlowdimlem13  29011  ex-dif  30481  ex-un  30482  ex-in  30483  ex-xp  30494  ex-cnv  30495  ex-rn  30498  ex-res  30499  spanpr  31639  superpos  32413  cnvprop  32757  brprop  32758  mptprop  32759  coprprop  32760  prct  32774  prodpr  32887  ccfldextdgrr  33804  esumpr  34198  eulerpartgbij  34504  signswch  34693  prodfzo03  34735  subfacp1lem1  35349  altopthsn  36131  onint1  36619  bj-prexg  37334  bj-prex  37335  bj-prfromadj  37340  poimirlem8  37937  poimirlem9  37938  poimirlem15  37944  smprngopr  38361  dihprrnlem1N  41858  dihprrnlem2  41859  djhlsmat  41861  lclkrlem2c  41943  lclkrlem2v  41962  lcfrlem18  41994  pr2dom  43942  dfrcl4  44091  iunrelexp0  44117  corclrcl  44122  corcltrcl  44154  cotrclrcl  44157  mnuprdlem2  44688  sumpair  45454  rnfdmpr  47717  perfectALTVlem2  48186  usgrexmpl2edg  48493